Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code check failed for Haskell:

Email Gateway (Dec 28 2024 at 17:14):

From: Tobias Nipkow <nipkow@in.tum.de>
When building AFP/devel/Collections:

Collections FAILED (see also "isabelle build_log -H Error Collections")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls -XRankNTypes
-XScopedTypeVariables -odir build -hidir build -stubdir build -e ""
Generated_Code.hs
*** At command "export_code" (line 90 of
"$AFP/Collections/ICF/tools/Locale_Code_Ex.thy")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls -XRankNTypes
-XScopedTypeVariables -odir build -hidir build -stubdir build -e ""
Generated_Code.hs
*** At command "export_code" (line 1095 of "$AFP/Collections/Lib/Diff_Array.thy")

What is happening here? How can I avoid this?

I am on AFP c69ba7047b69 and isabelle 4219bb3951de

Thanks
Tobias

PS I know isabelle-dev is the correct destination but I am having problems with
that one.

smime.p7s

Email Gateway (Dec 28 2024 at 20:36):

From: Tobias Nipkow <nipkow@in.tum.de>
Florian,

That seems to have been the problem. I have backed out that changeset and pushed
that.

Tobias

On 28/12/2024 19:09, Florian Haftmann wrote:

Hi Tobias,

Am 28.12.24 um 18:13 schrieb Tobias Nipkow:

When building AFP/devel/Collections:

Collections FAILED (see also "isabelle build_log -H Error Collections")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls -
XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e
"" Generated_Code.hs
*** At command "export_code" (line 90 of "$AFP/Collections/ICF/tools/
Locale_Code_Ex.thy")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls -
XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e
"" Generated_Code.hs
*** At command "export_code" (line 1095 of "$AFP/Collections/Lib/
Diff_Array.thy")

What is happening here? How can I avoid this?

I am on AFP c69ba7047b69 and isabelle 4219bb3951de

it might be related to some extension I made recently in https://isabelle-
dev.sketis.net/rISABELLE0ca0a47235e53ec93bce681e2a149726b829db61 – although
isabelle build_task reported no issues (maybe I accidentally checked the wrong
points in history?).

Unfortunately I am currently away from anything and can’t check myself what’s
going on. Feel free to back out the changeset 0ca0a47235e5 (hg backout) and if
that helps, push that also.

PS I know isabelle-dev is the correct destination but I am having problems
with that one.

Me too, I made a new account using my @cit.tum.de mail address. Maybe this is
related of the enforced turning down of well-established domains like
informatik.tu-muenchen.de…

Cheers,
    Florian

smime.p7s

Last updated: Jan 04 2025 at 20:18 UTC