Email Gateway (Mar 06 2021 at 00:30): Email Gateway (Mar 06 2021 at 00:30):From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,
I am trying to get Isabelle2021 working on NixOS. Due to filesystem
layout, downloading binaries doesn't really work on NixOS, so this
involves packaging Isabelle, with some external dependencies.
However, we do match the version of polyml exactly:
polyml = polyml.overrideAttrs (attrs: {
configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];
version = "for-isabelle";
src = fetchFromGitHub {
owner = "polyml";
repo = "polyml";
rev = "f86ae3dc168612d51e7a73fbe3b7e02cb3bc1bac";
sha256 = "09f28jz6mnb4c0r1v57cwyw2vcwhdq57v6c5j8kwn2640cfl1gz7";
};
});
Nevertheless, building Pure results in this quite curious error:
Error: Value or constructor (buildCall3) has not been declared in structure Foreign
Foreign.buildCall3
(
Foreign.getSymbol (Foreign.loadLibraryIndirect (fn ...)) "sha1_buffer",
(Foreign.cByteArray, Foreign.cUlong, ...),
Foreign.cPointer
)
At (line 152 of "General/sha1.ML")
Error: Value or constructor (getSymbol) has not been declared in structure Foreign
Foreign.buildCall3
(
Foreign.getSymbol (Foreign.loadLibraryIndirect (fn ...)) "sha1_buffer",
(Foreign.cByteArray, Foreign.cUlong, ...),
Foreign.cPointer
)
At (line 153 of "General/sha1.ML")
[...]
I'm not sure what's going on here. There were some changes in the commit
range between 5.8.1 and this pinned commit involving libffi, but the
Poly/ML sources distributed with Isabelle don't seem to include any
workarounds; diff claims there's no difference.
I confirmed that referring to Foreign.buildCall3 in a REPL triggers the
error in the new Poly but not in 5.8.1.
Any insights on why this might be happening? Perhaps this was already
encountered when updating the Poly/ML in use by Isabelle?
Kind regards,
Jakub Kądziołka
Email Gateway (Mar 06 2021 at 23:16):From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,
I have figured out what the problem was. We were building PolyML by
running 'make', instead of running 'make compiler' twice like Isabelle
does. This seems to have had some weird consequences for bootstrapping.
Regards,
Jakub Kądziołka
Last updated: Apr 16 2024 at 08:18 UTC