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



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

On Tue, Apr 24, 2018 at 11:44 AM Makarius <makarius at sketis.net> wrote:

> 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
>



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