Email Gateway (Aug 18 2022 at 17:30): Email Gateway (Aug 18 2022 at 17:30):From: Anh Le <anhlevn@cims.nyu.edu>
Hi everyone,
Is there any way that we can use Isabelle/Isar as a compiler?
For example, how do we run a command like:
$ ./isabelle MyTheory.thy
And then isabelle will do as the Proof General processes the whole buffer,
and will return the first found error if it exists.
Thank you
Email Gateway (Aug 18 2022 at 17:30):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi,
the corresponding command is
isabelle usedir -b HOL Name-of-output-Heap
reading the name of the used theory from the file ROOT.ML. In your case
this should contain:
use_thys ["MyTheory"];
In the above command, HOL is the name of the underlying heap image und
the last argument is the name which you choose for the resulting heap image.
For a detailed description see the isabelle system manual, i.e.,
isabelle doc system
(starting on page 20 in the documentation for Isabelle2011).
cheers
chris
Email Gateway (Aug 18 2022 at 17:31):From: Sree Harsha Totakura <totakura@in.tum.de>
Recently I wrote a small expect script to do the same, it is attached along
with this mail. It uses the Isabelle tty tool. You should copy (don't link)
it to your isabelle_home/bin directory where the 'isabelle' script resides.
The script needs 'expect' tool to be present in /usr/bin/
You can use this tool by passing your theory file as an argument. If
successful it returns 0 else 1.
Ex: bin/thm-validator test.thy
Regards,
Sree Harsha Totakura
Technische Universität München
thm-validator
Last updated: Apr 19 2024 at 01:05 UTC