Email Gateway (Aug 22 2022 at 13:23): Email Gateway (Aug 22 2022 at 13:23):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear all,
I am reviewing a paper which includes an Isabelle/HOL 2005
formalization and I want to verify the formalization myself. The
formalization consists of six files xxx.{thy,ML}, yyy.{thy,ML} and
zzz.{thy,ML}. I have no prior experience with the Isabelle proof
assistant.
Three questions:
How do I install Isabelle/HOL 2005 and use it to verify the
formalization? My available platforms are OS X and Linux.
My background in interactive theorem proving is with Coq. In Coq one
can add additional axioms in one's formalization. Can one do something
similar in Isabelle/HOL and if so how do I check what (if any) axioms
have been added? (That is, how do I check that the authors of the
paper have not "cheated" in their proofs.)
Anything else I should think of?
Best regards,
Anonymous Reviewer
Email Gateway (Aug 22 2022 at 13:26):From: Makarius <makarius@sketis.net>
As a long-standing release manager of Isabelle, I want to take the
opportunity to point out some tautologies:
* Only the latest Isabelle release is officially supported.
* The last 2-3 Isabelle releases may still work without further ado,
and people are welcome to ask questions about them on this mailing list
(when they say explicitly which version they mean).
* Much older Isabelle versions often do not work on current operating
systems. This is perfectly normal for a complex system that is merely
"archived" (according to the terminology on the Isabelle website), but
not actively maintained over time.
Note that companies like Oracle ask $$$ to continue particular Java
versions over more than 2 years, for customers who are incapable to get
onto release trains.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC