Email Gateway (Aug 22 2022 at 13:16): Email Gateway (Aug 22 2022 at 13:16):From: Rajeev Gore <Rajeev.Gore@anu.edu.au>
Dear Anonymous Reviewer,
please see the files at the URL
http://users.cecs.anu.edu.au/~jeremy/tmp/
Issue (1) - use of an old version of Isabelle. This was a new version
once, when I first did proofs in this area. Unfortunately new
versions are highly incompatible, like a different prover with the
same name, so I'm stuck with the old one. As the reviewer has
discovered, the developers have also at some time stopped making the
2005 version and installation instructions available on their archive.
However I have just installed it on a borrowed computer in London,
running Linux, with the following details:
Linux robotpc3-temp.cs.ucl.ac.uk 3.6.11-4.fc16.i686.PAE #1 SMP Tue Jan 8 21:18:14 UTC 2013 i686 i686 i386 GNU/Linux
So here are instructions for what I did (from memory, unfortunately,
as the computer I've borrowed erases user files on reboot(!)).
That computer does have 32-bit libraries installed!
Doing (from the directory where you unpack polyml-4.1.4.tar) cd
polyml-4.1.4/x86-linux ldd poly may make it clear whether you need to
install them
Go to
http://users.cecs.anu.edu.au/~jeremy/isabelle/
Download Isabelle2005.tar and polyml-4.1.4.tar
Choose a directory to work (it's /home/users/jeremy in my own case)
Put the tar files into that directory and unpack them (tar xvf filename.tar)
In Isabelle2005/etc/settings you need to edit it by changing
/home/users/jeremy to whatever directory you have chosen to use
Then type
/home/users/jeremy/Isabelle2005/bin/isabelle (changed as necessary).
which should start Isabelle 2005
If this works you can type
[sym, refl, trans] ;
and it will display the text of those three theorems.
For the specific work of the paper you need to download a lot of files from
http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/
Easiest to download just gen.tar and unpack it, to create a whole lot of files
in your directory (which you need to create) isabelle/2005/gen/
(or choose another directory if you like)
Get into this directory and start Isabelle as above by
/home/users/jeremy/Isabelle2005/bin/isabelle (changed as necessary).
Then
use_thy "tripartite" ;
should run a lot of preliminary proofs then the results of the paper
(of which the last is wf_rearr_n)
Issue (2) - the url in the paper had not been updated. Mea culpa.
What can I say, except that it's my fault, not my co-authors'.
And to compliment the referee(s) - I think most don't try to check on the
proof files. Of course it's just Murphy's Law that this happens when I'm
not able to fix it right away. And I'm sorry if the half-baked attempts to
fix it by email led to wasting more of their time.
Issue (3) - this theorem is the last in tripartite.ML, and the last
to show when
Email Gateway (Aug 22 2022 at 13:25):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Anonymous Reviewer,
my apologies for my tardiness in replying. I would usually ask Jeremy
Dawson to answer your question but he is traipsing around Europe
somewhere on a well-deserved holiday with his wife, and is unable to
help.
I tried to install Isabelle2005 myself to no avail. Apparently there
is something wrong with the "build" script and it is unable to find
the right files. I have searched on the web and found some relevant
links, but nothing that allows the installation to complete.
Jeremy suggested that I just copy his Isabelle2005 directory to my
public home page and send you the link, so I have done that. It is at:
http://users.cecs.anu.edu.au/~rpg/Isabelle2005.tar.gz
I am afraid that this is the best that I can do for now.
best wishes,
raj
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Email Gateway (Aug 22 2022 at 13:26):From: Rajeev Gore <Rajeev.Gore@anu.edu.au>
Dear Anonymous reviewer,
Jeremy has suggested that I also put up the polyml directory and a
repaired script which works for Jeremy. So here they are:
http://users.cecs.anu.edu.au/~rpg/polyml-4.1.4.tar.gz
http://users.cecs.anu.edu.au/~rpg/settings
The file "settings" has to live in this directory:
Isabelle2005/etc/
For me, the fixed script still causes a segmentation fault.
best wishes,
raj
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Email Gateway (Aug 22 2022 at 13:26):From: Makarius <makarius@sketis.net>
We are back to the running gag on this mailing list: inappropriate use
of the word "fixed".
The situation: some archeological Isabelle version is put into a current
operating system context. After more than a decade, it is to be expected
that certain things no longer work. This is not a problem of that
Isabelle version, but of the OS context (or the user expecting it to
work without continued maintenance).
The canonical solution (invented by IBM in the 1960/1970s): set up a
virtual machine that runs some Linux version from 2004/2005 (e.g. SuSE).
Everything should work out of the box, just as in 2005 when Isabelle2005
was published.
Makarius
Last updated: Apr 30 2024 at 08:19 UTC