I am trying to get Isabelle2019 running on NixOS. I used the nix expression from nixpgs (https://github.com/NixOS/nixpkgs/blob/5e2f89bbce11069748e35830f51b3bd9a45c871c/pkgs/applications/science/logic/isabelle/default.nix) where I replaced the directory *contrib/java/* by *contrib/java-** and changed the version to *2019*. I also switched to polyml-5.8 using the nix expression https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/compilers/polyml/default.nix. When trying to build Pure on startup of Isabelle, I get the following errors:

At (line 27 of "General/integer.ML") Error: Structure does not match signature. Signature: val div_mod: int -> int -> int * int Structure: val div_mod: IntInf.int -> IntInf.int -> IntInf.int * IntInf.int Reason: Can't match IntInf.int (*In Basis*) to int (*In Basis*) (Different type constructors) struct fun min x ... = Int.min (...) fun max ... = ... ... fun add ... = ... fun ... fun ... ... ... end At (line 27 of "General/integer.ML") Error: Structure does not match signature. Signature: val gcd: int -> int -> int Structure: val gcd: LargeInt.int -> LargeInt.int -> LargeInt.int Reason: Can't match LargeInt.int (*In Basis*) to int (*In Basis*) (Different type constructors) struct fun min x ... = Int.min (...) fun max ... = ... ... fun add ... = ... fun ... fun ... ... ... end At (line 27 of "General/integer.ML") Exception- Fail "Static Errors" raised Exception- ERROR "ML error" raised Error trying to use the file: 'ROOT.ML'

Does anybody have an idea what the cause could be?

Probably a mismatch of Poly/ML versions.

I found the issue! Poly/ML has to be compiled with the *--enable-intinf-as-int* flag.

Last updated: Dec 07 2023 at 08:19 UTC