Email Gateway (Aug 22 2022 at 17:01): Email Gateway (Aug 22 2022 at 17:01):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
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
Email Gateway (Aug 22 2022 at 17:07):From: Makarius <makarius@sketis.net>
On 26/03/18 22:08, Mario Alvarez wrote:
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.
This thread is still open and unanswered, as far as I can see. After
reading the text two times, I can only guess what you are trying to do.
Although Coq and Isabelle have common heritage, and a lot of
similarities until today, there is a cultural gap to be bridged and one
of different terminology. E.g. "code extraction" in Coq (usually from
proofs) becomes "code generation" in Isabelle (from specifications).
Generally, Isabelle is more open and supports more languages within the
same framework: a standard approach is to use Isabelle/ML -- the meta
language around the logical environment -- to do parsing and I/O, but I
have occasionally seen people using Isabelle/HOL specifications as a
starting point and then generate ML or Haskell from it. (Maybe the
IsaFoR project can server as an example for that approach:
http://cl-informatik.uibk.ac.at/isafor).
As long as you stay inside Isabelle, everything happens in theory files
within a session (even Isabelle/ML). This explains why the documentation
of "isabelle process" in the "system" manual is relatively terse about
what you can do with it: loading theory files is the main operation
here. The same manual also documents "isabelle build" in chapter 2 --
that is the standard way to run Isabelle sessions without GUI front-end.
In principle, running an Isabelle session can do whatever you like, with
the help of some Isabelle/ML snippets around your formalization, but it
is going to be a bit heavy. A more light-weight way is the forthcoming
Isabelle server, see also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/msg00088.html
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.
This already sounds quite concrete. Are your sources available
somewhere? It would help to get an idea what are the missing bits.
Makarius
Email Gateway (Aug 22 2022 at 17:12):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
Hi Makarius,
Thanks for your response. Currently I am using extraction to OCaml, which
has been working OK so far for my purposes - in other words, switching from
the second approach I described in my prior email to the first one. (I've
built unverified OCaml shims to handle the I/O).
Also, thank you for the hint about IsaFoR as an example of using
Isabelle/ML to achieve these goals. I think for now using code extraction
to OCaml (I don't mean synthesizing code from proofs, I just mean
translating executable functions in Isabelle/HOL to executable OCaml
functions) will be a good approach for me as it will let people install my
compiler without installing all of Isabelle. I'll also take a look at the
Isabelle server to see if it meets any of my needs.
If you'd like to take a look at my sources, they are here (in a
subdirectory of my fork of Eth-Isabelle):
https://github.com/mmalvarez/eth-isabelle/tree/master/elle
(FourLExtract.thy and FourLShim.ml are probably the most relevant files).
Also, thanks for taking the effort to read and understand my last email
despite the ambiguities. As I get more acculturated to the Isabelle way of
doing and discussing things, hopefully I can improve my communications.
Many thanks,
Mario
Last updated: Apr 24 2024 at 08:20 UTC