This is on Agda 2.7.0, MAlonzo, on Debian Linux 12
installed by
$ cabal install -foptimise-heavily -j1,
lib-2.1
All the application modules are type-checked by type-checking CheckAll.agda.
CheckAll.agda consists of many lines of kind
open import Foo
And there is only one module in this list that applies the `main' function:
Pol.Univariate.KTest.
It is the example that uses other modules and needs to be compiled to executable.
Type checking:
$ agda $agdaLibOpt $agdaFlags CheckAll.agda +RTS -M12G
where
$agdaFlags = "--auto-inline --guardedness"
Compilation to executable example:
$ agda -c $agdaLibOpt $agdaFlags Pol/Univariate/KTest.agda +RTS -M12G
It reports
"
An internal error has occurred. Please report this as a bug.
Location of the error: IMPOSSIBLE_VERBOSE, called at src/full/Agda/
TypeChecking/Monad/Signature.hs:869:32 in
Agda-2.7.0-5b1c26af24f71478be7921bfd690317a6888da853b10d78f399aa31cab72a91e:
Agda.TypeChecking.Monad.Signature
"
Call the above approach (I).
a) In a strange way, this error does not appear for other executable examples set instead of Pol/Univariate/KTest.agda.
b) I also recall (not very surely) that Agda 2.6.4.3 is free of this effect.
c) There was some explanation about the effect, may be about year ago, which I did not understand.
Anyway, I apply the following approach instead.
Approach (II)(1) Start with only *.agda files of application.
Comment out in CheckAll.agda all the lines for the modules that have `main' .
This is only to remember the list of examples to be compiled separately.
(2) Type-check CheckAll.agda.
(3) Choose the needed example Foo.agda among the commented out lines and
command
$ agda -c ... Foo.agda
(4) Process other examples in this way by repeating (3) (without type-checking CheckAll.agda).
This compiles the examples correctly.
I write this because users will be frightened by this "internal error" message and will doubt of how to organize usage of their applications when such have examples to be compiled to executables.
I wonder of whether it is possible to fix Agda in such a way that the above effect would not appear at all.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4