Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Porting the Isabelle/HOL to a newer version


view this post on Zulip Email Gateway (Aug 19 2022 at 16:36):

From: Ghassen HELALI <helali@encs.concordia.ca>
Hello fellows
I wonder to know if there is any way to port an old Isabelle/HOL code to a
the newest version of Isabelle.
The old code is dated from the year 2000

Regards
--gh

view this post on Zulip Email Gateway (Aug 19 2022 at 16:36):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,

oh my dear, in which drawer has this been locked in all these years?

It is surely possible but will involve massive manual rephrasing. For a
more detailled statement a glimpse at the sources would be helpful.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 16:36):

From: Lawrence Paulson <lp15@cam.ac.uk>
14-year-old code won’t be easy to port. A precise answer to your question depends very much on what this code does, how big it is, and what parts of Isabelle it uses.

Larry Paulson

view this post on Zulip Email Gateway (Aug 19 2022 at 16:36):

From: "C. Diekmann" <diekmann@in.tum.de>
If it is actually no code (no ML) but primarily proof, you might be
(somewhat more) lucky. I see that there are afp entries dating back to
2003 [1], probably looking at their evolution could help (but this is
just a guess, ...).

Cornelius

[1] http://sourceforge.net/p/afp/afp-2003/ci/default/tree/thys/


Last updated: Mar 29 2024 at 04:18 UTC