Re: [isabelle] Code generation in the AFP



On 27/04/18 19:41, Makarius wrote:
> On 27/04/18 19:28, Lars Hupel wrote:
>>> Is that what I have described above or something else?
>>>
>>> The general idea is that "isabelle build" or Isabelle/jEdit sessions
>>> never write to the file-system -- that would be stateful -- but only to
>>> the stateless PIDE database.
>>
>> Sounds like it, yes. But just to clarify: is this a short- or long-term
>> solution?
> 
> Both short- and long-term, in a sense. Long-term, because the basic idea
> has been in the pipeline for a long time, in some form or another.
> Short-term, because it might actually happen really soon, if we are very
> lucky for the coming release.

I have already started working in that direction: see
Isabelle/ac82ee617a75 with the following NEWS entries:


*** ML ***

* Operation Export.export emits theory exports (arbitrary blobs), which
are stored persistently in the session build database.


*** System ***

* The command-line tool retrieves theory exports from the session build
database.


There are no applications yet. It is likely that there will be further
refinements, when it comes into practice.

I am presently also thinking in the direction to export proof terms
(without storing them in ML), maybe even OpenTheory output.


	Makarius




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