[isabelle] Examples of Extracting Isabelle/Running .thy Files as Scripts



Hi Isabelle-Users,

I'm currently trying to build a compiler in Isabelle, and trying to
determine what the best way to run the compiler is (i.e., to use the code
I've developed in Isabelle to transform concrete compiler inputs to
concrete compiler outputs, ideally using the command line.)

My understanding is that there are two (maybe more) ways to try to go about
doing this. One is what CompCert did - using an extraction mechanism to
build an ML version of the compiler, which can then be run (one downside to
this is that one also needs to implement a parser for input - the
equivalent of CompCert's *clightgen* utility).

The other is what was done in this paper
<https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/>,
where the proof assistant (again Coq) itself acts as the compiler, and the
output of running Coq files *as scripts* yields the desired output. In this
instance, Coq takes care of all the difficulties of parsing the input,
meaning the user only has to write programs inside the context of Coq ".v"
files.

I am attempting to do something similar to the second use-case for
Isabelle. However, I am struggling to figure out what the right way to do
this in Isabelle. Do you think it would be better to use extraction, or is
there a way I can run my .thy files as scripts to produce output? As far as
options for "running" .thy files, I can only see the "isabelle process"
command, which does not seem to be well documented and seems to struggle
with resolving dependencies.

Any good resources on ways to do this in Isabelle would be much
appreciated. Currently, the only way I have of running the compiler is in
JEdit, and I would really very much like a command-line interface for it.

Best,
Mario



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.