Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code check failed for Haskell:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Email Gateway (Jan 05 2025 at 21:55):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
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

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

view this post on Zulip Email Gateway (Jan 07 2025 at 10:37):

From: Fabian Huch <huch@in.tum.de>

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")
isabelle build_task reported no issues (maybe I accidentally checked
the wrong points in history?).

Note that clusterized builds do not have a Haskell environment, because
the underlying Build_Cluster does not support remote *_setup operations
for its nodes yet (and would ignore these components even if set up by
hand). This means that such code checks will be skipped (cf. the
'undefined ISABELLE_GHC' warnings in the log).

Fabian

view this post on Zulip Email Gateway (Jan 07 2025 at 15:05):

From: Fabian Huch <huch@in.tum.de>

On 1/7/25 11:29, Fabian Huch wrote:

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")
isabelle build_task reported no issues (maybe I accidentally checked
the wrong points in history?).

Note that clusterized builds do not have a Haskell environment,
because the underlying Build_Cluster does not support remote *_setup
operations for its nodes yet (and would ignore these components even
if set up by hand). This means that such code checks will be skipped
(cf. the 'undefined ISABELLE_GHC' warnings in the log).

Correction, now that the server is back online: There is indeed a
manually set up ISABELLE_GHC on there, since this one only depends on
accidental file system state -- other components (e.g. ISABELLE_GO)
require explicit management.

Fabian

view this post on Zulip Email Gateway (Jan 07 2025 at 15:58):

From: Makarius <makarius@sketis.net>
On 07/01/2025 16:05, Fabian Huch wrote:

Note that clusterized builds do not have a Haskell environment, because the
underlying Build_Cluster does not support remote *_setup operations for its
nodes yet (and would ignore these components even if set up by hand). This
means that such code checks will be skipped (cf. the 'undefined
ISABELLE_GHC' warnings in the log).

Correction, now that the server is back online: There is indeed a manually set
up ISABELLE_GHC on there, since this one only depends on accidental file
system state -- other components (e.g. ISABELLE_GO) require explicit management.

First note, that my plan for Isabelle2025-RC1 is to provide the missing
Other_Isabelle operations to do "isabelle go_setup" or "isabelle ghc_setup" on
the target environment, in a way that works for historic versions, too.

Further, I wonder what the uninformative test by Florian really looked like,
and if there were other reasons for the problem.

Many years ago, when we came up with the "isabelle ghc_setup" plan via
"stack", the overall prospect was more optimistic. In the meantime I've see
too many odd failures: the setup is not as well-defined or "statically
closed", as it should be. (GHC/Stack is much better than OCaml/OPAM, though.)

Makarius

view this post on Zulip Email Gateway (Jan 07 2025 at 19:37):

From: Florian Haftmann <florian.haftmann@cit.tum.de>

Note that clusterized builds do not have a Haskell environment,
because the underlying Build_Cluster does not support remote *_setup
operations for its nodes yet (and would ignore these components even
if set up by hand). This means that such code checks will be skipped
(cf. the 'undefined ISABELLE_GHC' warnings in the log).

Correction, now that the server is back online: There is indeed a
manually set up ISABELLE_GHC on there, since this one only depends on
accidental file system state -- other components (e.g. ISABELLE_GO)
require explicit management.

My check was to leave out the question mark after Haskell in

https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Codegenerator_Test/Generate.thy#l18

and schedule that as build task.

Now with that background information I am aware that this just worked by
accident.

So for the moment I will apply traditional build-all if needed.

Cheers,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: Feb 05 2025 at 16:23 UTC