Email Gateway (Jan 27 2026 at 18:22): Email Gateway (Jan 27 2026 at 18:22):From: Walther Neuper <cl-isabelle-users@lists.cam.ac.uk>
My installation (zipped in the attachment) is still not perfect. According to isar-ref.pdf I did:
../principles_financing$ /usr/local/Isabelle2025-2/bin/isabelle mkroot -I
.. complete root.tex
../principles_financing$ /usr/local/Isabelle2025-2/bin/isabelle build -D .
Text written in Principles_Financing.thy I would like to see in ../principles_financing/output/document.pdf, but there are only data fetched (correctly) from ../principles_financing/document/root.tex and none from Principles_Financing.thy.
What is missing for a perfectly working installation?
Email Gateway (Jan 27 2026 at 18:47):From: Makarius <makarius@sketis.net>
On 26/01/2026 09:59, Walther Neuper (via cl-isabelle-users Mailing List) wrote:
My installation (zipped in the attachment) is still not perfect. According to
isar-ref.pdf I did:../principles_financing$ /usr/local/Isabelle2025-2/bin/isabelle mkroot -I
.. complete root.tex
../principles_financing$ /usr/local/Isabelle2025-2/bin/isabelle build -D .Text written in Principles_Financing.thy I would like to see in ../
principles_financing/output/document.pdf, but there are only data fetched
(correctly) from ../principles_financing/document/root.tex and none from
Principles_Financing.thy.What is missing for a perfectly working installation?
Walther,
I am pretty sure that you did not intend to post private documents on the
isabelle-users mailing list --- presumably it was an accidental reply to one
of my recent postings.
Luckily there is no content yet, apart from minimal meta-data.
The reason why you don't see and content of the theory is the initial
meta-comment (<) --- which is not even properly balanced by (>) --- and
apparently this ancient left-over feature does not care. The last time I've
revised that was in 2005.
Side-remark: sending around drafts via email is generally bad version
management. There should be a proper source repository somewhere, preferably
in a private space.
Makarius
Last updated: Jan 31 2026 at 12:53 UTC