[Agda] Agda 2.7.0 release candidate 1

[mechvel at scico.botik.ru]

On 2024-07-14 20:37, Andreas Abel wrote:
> Dear all,
> 
> The Agda Team is pleased to announce a release candidate for Agda 
> 2.7.0.
> [..]

I test it on  lib-2.1-rc2, MAlonzo, ghc-9.02, Debian 12,
installing it with
$ cabal install -foptimise-heavily -j1
by applying
$ agda $agdaLibOpt $agdaFlags CheckAll.agda +RTS -M12G,
where
$agdaFlags =  --auto-inline --guardedness,

$ agda -c $agdaLibOpt $agdaFlags --ghc-flag="-rtsopts" Nat/Test1.agda 
+RTS -M12G

1) It type-checks all my large library.
2) It compiles and runs  Test1  all right.

But
$ agda -c $agdaLibOpt $agdaFlags Pol/Test2.agda +RTS -M12G
reports
"
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__,
called at src/full/Agda/TypeChecking/Reduce.hs:224:18 in 
Agda-2.6.20240714-2fe3b1061e5ba2f2b4b6f08c27c282c63059624c784530918895e3dbeed5f51f:
Agda.TypeChecking.Reduce
"
Many modules are involved in both tests, but Test2 uses considerably 
more modules than Test1.
If you do not guess of the error reason, I could try to reduce the 
example.
But I fear it will still remain large. I doubt.

--
SM