Jan van Brügge (Feb 24 2021 at 14:49): Jan van Brügge (Feb 24 2021 at 14:49):Is there a place where I can still get the Isabelle2020 download? I tried 2021 just now by updating with the AUR package, but Nominal2 is broken:
Building Nominal2 ...
Nominal2 FAILED
(see also /opt/isabelle/heaps/polyml-5.8.2_x86_64_32-linux/log/Nominal2)
*** ML error (line 118 of "~~/src/Nominal2/nominal_dt_rawfuns.ML"):
*** Value or constructor (subtarget) has not been declared in structure Local_Theory
*** ML error (line 255 of "~~/src/Nominal2/nominal_dt_rawfuns.ML"):
*** Value or constructor (subtarget) has not been declared in structure Local_Theory
*** ML error (line 328 of "~~/src/Nominal2/nominal_dt_rawfuns.ML"):
*** Value or constructor (subtarget) has not been declared in structure Local_Theory
*** At command "ML_file" (line 13 of "~~/src/Nominal2/Nominal2.thy")
Unfinished session(s): Nominal2
https://isabelle.in.tum.de/website-Isabelle2020/
Jan van Brügge (Feb 24 2021 at 15:02):Thank you, yes that did work
Manuel Eberl (Feb 24 2021 at 15:25):Nominal2 works fine for me. Did you upgrade to AFP2021?
Manuel Eberl (Feb 24 2021 at 15:26):(Also I wouldn't recommend packages like those from the AUR. There have been various problems with them in the past.)
Jannis Harder (Feb 27 2021 at 07:57):FWIW the AUR package just takes the Isabelle binary release and sticks it into /opt/isablle unmodified, so I don't expect any of the problems that other packaging efforts have that build Isabelle themselves or even try to make it use system dependencies
Jan van Brügge (Mar 01 2021 at 12:46):Did you upgrade to AFP2021?
This was my error. I did not read the "old versions" bit, and just saw that 2020 was the newest version in the list and did not think that "download this entry" would give me a version not in the list
Last updated: Dec 21 2024 at 12:33 UTC