Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 05.02.19 13:18, Salomon Sickert wrote:




It should be easy to make this part of the formal session, with some
options [condition = ISABELLE_MLTON].

The 'export_code' command will have to emit generated files
(Generated_Files.add_files) to make the assembly work in Isabelle/ML.

I have already added support for executable exports in
Isabelle/c175499a7537 -- a few more such fine-tunings might be required.


Could someone point me to an example on how to do compilation with either mlton 
or polyml within a formal session?
The build scripts in these two entries are copying the style of the CAVA entry 
at that time and I’m not sure about the current best practices here.


A partial example with generated files is src/Tools/Haskell/Test.thy 
(e.g. in Isabelle/2c3e5e58d93f): the generated Haskell sources are used 
for a test build, but its result is thrown away instead of exporting it.


I have some ideas in the pipeline to make the 'export_files' 
specifications in session ROOT entries more robust (no export by 
default) and more useful (collective export on something like "isabelle 
build -e").



We also need to wait for Florian Haftmann to provide the 
Generated_Files.add_files facility to 'export_code' -- in parallel to 
its existing Export.export. The main difference that this will be an 
update on the theory.



(Note that I am presently busy elsewhere and only sporadically connected.)

Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Salomon Sickert]

>> To add a couple more to the list:
>> 
>> — LTL has includes a parser that is used in an example and built using 
>> LTL/examples/build_poly.sh
>> 
>> — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh 
>> and LTL_to_DRA/Code/build_mlton.sh
> 
> It should be easy to make this part of the formal session, with some
> options [condition = ISABELLE_MLTON].
> 
> The 'export_code' command will have to emit generated files
> (Generated_Files.add_files) to make the assembly work in Isabelle/ML.
> 
> I have already added support for executable exports in
> Isabelle/c175499a7537 -- a few more such fine-tunings might be required.

That is a great development. 

Could someone point me to an example on how to do compilation with either mlton 
or polyml within a formal session?
The build scripts in these two entries are copying the style of the CAVA entry 
at that time and I’m not sure about the current best practices here.

Best,
Salomon
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 01/02/2019 15:30, Lars Hupel wrote:
> 
> – Sturm_Sequences produces some extra LaTeX documentation. The generated
> PDF is even committed to the AFP.
> 
>>   * no generated files in the repository (these are not sources but
>> results from sources)

See now

changeset:   10104:394951259923
user:wenzelm
date:Mon Feb 04 16:42:52 2019 +0100
files:   thys/Sturm_Sequences/ROOT
thys/Sturm_Sequences/document/build
thys/Sturm_Sequences/document/root_userguide.tex
thys/Sturm_Sequences/guide/Makefile thys/Sturm_Sequences/guide/guide.pdf
thys/Sturm_Sequences/guide/guide.tex
thys/Sturm_Sequences/guide/isabelle.eps
thys/Sturm_Sequences/guide/isabelle.pdf
description:
proper Isabelle document setup, without generated files in the repository;


It means that the document will also show up in the generated HTML,
similar to the userguide in AFP/Collections.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 04/02/2019 08:00, Salomon Sickert wrote:
> 
> 
> To add a couple more to the list:
> 
> — LTL has includes a parser that is used in an example and built using 
> LTL/examples/build_poly.sh
> 
> — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh 
> and LTL_to_DRA/Code/build_mlton.sh

It should be easy to make this part of the formal session, with some
options [condition = ISABELLE_MLTON].

The 'export_code' command will have to emit generated files
(Generated_Files.add_files) to make the assembly work in Isabelle/ML.

I have already added support for executable exports in
Isabelle/c175499a7537 -- a few more such fine-tunings might be required.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Salomon Sickert]

> On 1. Feb 2019, at 15:30, Lars Hupel  wrote:
> 
>> What are the remaining uses of these? How much of this can be integrated
>> into the formal Isabelle session? How much of it is actually obsolete?
> 
> Hard to tell from a distance, but here's what I gather from reading the
> Makefiles:
> 
> – Formal_SSA appears to download some file, unpack it, and compile
> generated code together with it.
> 
> – Lightweight_Java generates an Isabelle theory file with Ott.
> 
> – Buchi_Complementation compiles generated code with MLton.
> 
> – Sturm_Sequences produces some extra LaTeX documentation. The generated
> PDF is even committed to the AFP.

To add a couple more to the list:

— LTL has includes a parser that is used in an example and built using 
LTL/examples/build_poly.sh

— LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh and 
LTL_to_DRA/Code/build_mlton.sh

Best,
Salomon

>>  * no generated files in the repository (these are not sources but
>> results from sources)
> 
> What about generated theory files? This also affects the CakeML entry. I
> could easily package Lem as a component, but how would "isabelle build"
> call it?
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 02/02/2019 14:13, Florian Haftmann wrote:

> * The module naming schema gets more sophisticated: default, name or
> prefix.  The key point is that this naming schema is again
> target-language specific.

Just abstractly, a reform should strive for unification and
simplification whenever possible.

The different languages have slightly different side-conditions, but
maybe they can still be unified: e.g. the main NAME could become
NAME.EXT or NAME/ depending on the situation.

One could also use the const names to produce a default, e.g. according
to the traditional scheme to concatenate const base names with "_" as
separator.


> This should cover all application cases.

When export_code emits Generated_Files.add_files, there is always a
possibility to do special-purpose Isabelle/ML programming with
Generated_Files.get_files. No need to have all odd cases in one Isar
command.


> At the moment I am still in favour of a diagnostic command to emit sth
> ad-hoc into the file system -- but this could be something separate from
> export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination.

For diagnostics I have used the "isabelle-export:" VFS in Isabelle/jEdit
so far: if a physical file is required, it can be written from the
editor (which actually cased the crash before Isabelle/9fd395ff57bc).

Minor disadvantage: writing directory content is inconvenient. In that
case there is also Generated_Files.write_files.


Some months ago I've seen odd crashes with files written to
$ISABELLE_TMP_PREFIX/ in Isabelle/ML and read in Isabelle/Scala.
Moreover I've seen crashes of the Headless PIDE session of export_code
with $ISABELLE_TMP_PREFIX in particular.

There might be something wrong in my areas of responsibility, or
something inherently fragile in concurrent access to a Unix file-system.

These incidents motivated to revive the pending thread to eliminate
physical files from export_code in the first place. Mathematical files
in the theory context are more reliably than physical ones on a magnetic
drum.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Florian Haftmann]

>> Maybe the »checking« should just be a variant of the regular export.
>>
>> Hence the modification could be quite conservative:
>>
>>  export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
>> ( file … | ( prefix … ) ( checked ) )
>>
>> where »file« denotes a relative root in the file system and »checked«
>> indicated that the generated code will be checked implicitly.
> 
> I have looked around at typical uses of 'export_code' in AFP. Most of
> the time it is just informative: writing a file and looking at it in the
> editor (or via the command-line!?), or doing that on the output channel.
> The isabelle-export: file-system covers that already, i.e. we should be
> able to eliminate almost all generated files from the AFP repository.
> 
> So "export_code .. file" should just disappear -- it is semantically
> illtyped in PIDE: editing the "file" argument will leave a trace of
> machine oil spilled to the physical file-system.
> 
> 
> We do need an explicit prefix and an internal check for duplicates, e.g.
> as in the command 'generated_file'.
> 
> That should be really just a prefix for the exported artifact, not the
> name itself: each language processor should be smart enough to derive
> file or directory names from it as required.  Thus the prefix locally
> belongs in front of the arguments.
> 
> Here is an example from AFP/160ac13cdc05
> SATSolverVerification/SatSolverCode.thy:
> 
>   export_code solve
> in OCaml file "code/solve.ML"
> in SML file "code/solve.ocaml
> in Haskell file "code/"
> 
> It could be turned into something like this:
> 
>   export_code "code/" = solve in OCaml SML Haskell
> 
> Some details about the automatic name derivation scheme still need to be
> sorted out -- or 'file' remains as an option to specify the suffix for
> effective name (without writing anything to the file-system).

Some further round of thinking.  Indeed, naming files is a little bit
delicate since there are two classes of target languages here: Haskell
with its strict one module – one file approach and ML where source code
is conceptually just a stream.  Hence in the current implementation the
exact interpretation of the »file« argument is up to the target language.

To make this more fitting, at the moment I am thinking about something like

> export_code [ ( NAME | PREFIX._ ) = ] CONSTS in LANGUAGE [ '(' OPTIONS ')' ] 
> [ file_prefix PATH ] [ checked ] 

* »checked« is just an aside to regular code generation, no distinctive
variant

* A mere prefix for the relative location can be given after »file_prefix«.

* Language-specific options remain as they are.

* The module naming schema gets more sophisticated: default, name or
prefix.  The key point is that this naming schema is again
target-language specific.

  For ML:
   code   file name
  default  multiple structurestheory name
  name one structure NAME NAME
  prefix   one structure PREFIX with multiple structures  PREFIX

  For Haskell:
   codefile name
  default  multiple modulesmodule name
  name one module NAME NAME
  prefix   multiple modules beneath PREFIX PREFIX module name

This should cover all application cases.

It will take further rounds of refinement to actually get there.

At the moment I am still in favour of a diagnostic command to emit sth
ad-hoc into the file system -- but this could be something separate from
export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination.

Just an aside: with the current tool support in Isabelle/jEdit I
consider the auxiliary construct »file ‹›« obsolete – the regular
exports are just two clicks away.

Cheers,
Florian



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 01/02/2019 16:40, Lars Hupel wrote:
>> The standard approach for the latter is to have the other tool directly
>> import its source format into the theory context within Isabelle/ML,
>> without the intermediate theory source. Doing this carefully, would even
>> produce nice PIDE markup for the original sources. PIDE is an IDE for
>> arbitrary user-defined languages.
>>
>> It might be worth doing this for tools like Lem eventually, but I have
>> not looked at it closely so far.
> 
> Lem is implemented in OCaml, so this seems like a stretch. I'd say
> importing HOL4 into Isabelle is a more plausible solution.

Yes, the motivation behind using Lem is diminished by the promising work
of Fabian Immler.

In general, though, alien tool output can be imported into the formal
context. One merely needs to devise some tricks. A tool implemented in
Haskell or OCaml should be particularly easy.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> The standard approach for the latter is to have the other tool directly
> import its source format into the theory context within Isabelle/ML,
> without the intermediate theory source. Doing this carefully, would even
> produce nice PIDE markup for the original sources. PIDE is an IDE for
> arbitrary user-defined languages.
> 
> It might be worth doing this for tools like Lem eventually, but I have
> not looked at it closely so far.

Lem is implemented in OCaml, so this seems like a stretch. I'd say
importing HOL4 into Isabelle is a more plausible solution.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 01/02/2019 15:30, Lars Hupel wrote:
> 
>>   * no generated files in the repository (these are not sources but
>> results from sources)
> 
> What about generated theory files? This also affects the CakeML entry. I
> could easily package Lem as a component, but how would "isabelle build"
> call it?

The present reform is mainly about generated output files, not input
theory files.


The standard approach for the latter is to have the other tool directly
import its source format into the theory context within Isabelle/ML,
without the intermediate theory source. Doing this carefully, would even
produce nice PIDE markup for the original sources. PIDE is an IDE for
arbitrary user-defined languages.

It might be worth doing this for tools like Lem eventually, but I have
not looked at it closely so far.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> What are the remaining uses of these? How much of this can be integrated
> into the formal Isabelle session? How much of it is actually obsolete?

Hard to tell from a distance, but here's what I gather from reading the
Makefiles:

– Formal_SSA appears to download some file, unpack it, and compile
generated code together with it.

– Lightweight_Java generates an Isabelle theory file with Ott.

– Buchi_Complementation compiles generated code with MLton.

– Sturm_Sequences produces some extra LaTeX documentation. The generated
PDF is even committed to the AFP.

>   * no generated files in the repository (these are not sources but
> results from sources)

What about generated theory files? This also affects the CakeML entry. I
could easily package Lem as a component, but how would "isabelle build"
call it?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 01/02/2019 14:29, Lars Hupel wrote:
>> In 2012 we eliminated all Makefiles from AFP: I did not know that some
>> came back, or chose to ignore it.
> 
> ~/work/afp (default)$ find thys/ -name Makefile
> thys/Buchi_Complementation/code/Makefile
> thys/Formal_SSA/Makefile
> thys/LightweightJava/ott-src/Makefile
> thys/Sturm_Sequences/guide/Makefile

What are the remaining uses of these? How much of this can be integrated
into the formal Isabelle session? How much of it is actually obsolete?


We have plenty of mechanisms in "isabelle build" (and "isabelle
process") that are waiting to be put into proper use.

>From a maintenance point of view the goals are:

  * no generated files in the repository (these are not sources but
results from sources)

  * no violations of the stateless PIDE model, e.g. commands that leave
a trace of garbage in the natural environment while editing (such as
"export_code ... file ..." with varying file names).


In principle, everything should work on a read-only file-system.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> In 2012 we eliminated all Makefiles from AFP: I did not know that some
> came back, or chose to ignore it.

~/work/afp (default)$ find thys/ -name Makefile
thys/Buchi_Complementation/code/Makefile
thys/Formal_SSA/Makefile
thys/LightweightJava/ott-src/Makefile
thys/Sturm_Sequences/guide/Makefile

> The formal status of sessions is defined via "isabelle build" -- that is
> a powerful tool that can do many things. I.e. we can easily define that
> anything outside of it as outside of AFP.

This is the de-facto situation, yes.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 01/02/2019 12:43, Lars Hupel wrote:
> 
> It would like to reiterate that the technical part of this issue is the
> easy bit. The difficult bit is deciding policy: Should Isabelle
> committers be responsible for breakage in downstream artifacts? In other
> words, should the AFP stability guarantees be extended? Right now we
> have that odd situation where extra sources are present (e.g. Makefiles)
> but nobody bothers to look at them.

In 2012 we eliminated all Makefiles from AFP: I did not know that some
came back, or chose to ignore it.

The formal status of sessions is defined via "isabelle build" -- that is
a powerful tool that can do many things. I.e. we can easily define that
anything outside of it as outside of AFP.

As usual, the empirical proof of this claims works by going through the
applications seen in practice, and to reform them to make them fit to
the model. (This sometimes requires minor adjustments of the model.)


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Lars Hupel]

> 1. Gratchk is a similar use-case, where I need to export code, link it
> with some external ML code using MLton b/c it's faster, and test the
> result for timing regressions. Because gratchk is also bundled with
> gratgen, which is implemented in C++, I have not yet put it into the
> AFP, b/c that would mean to separate gratchk from gratgen, or to push
> C++ code to the AFP, for which I cannot expect an build infrastructure
> there.
> 
> 2. In the AFP, there is the CAVA model checker. It also comes with some
> external ML code. I just checked, and this external ML code is already
> severely bit-rotten, as it has not been maintained for years now ... at
> latest the recent string-literal reform should have reliably killed it.
>  
> Also, timing regression tests are important when doing such reforms as
> the above-mentioned string-literal reform, which has the potential to
> severely slowdown the generated code.

This is not a new problem. It is merely slightly exacerbated by making
it more difficult to run such tests manually. There have been various
discussions about this in the past, but they are all orthogonal to the
issue of code generation.

It would like to reiterate that the technical part of this issue is the
easy bit. The difficult bit is deciding policy: Should Isabelle
committers be responsible for breakage in downstream artifacts? In other
words, should the AFP stability guarantees be extended? Right now we
have that odd situation where extra sources are present (e.g. Makefiles)
but nobody bothers to look at them.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Peter Lammich]

Can you give some more details on how to achieve this?
> 
> Concrete application: I have a verified SAT solver (lets call that 


1. Gratchk is a similar use-case, where I need to export code, link it
with some external ML code using MLton b/c it's faster, and test the
result for timing regressions. Because gratchk is also bundled with
gratgen, which is implemented in C++, I have not yet put it into the
AFP, b/c that would mean to separate gratchk from gratgen, or to push
C++ code to the AFP, for which I cannot expect an build infrastructure
there.

2. In the AFP, there is the CAVA model checker. It also comes with some
external ML code. I just checked, and this external ML code is already
severely bit-rotten, as it has not been maintained for years now ... at
latest the recent string-literal reform should have reliably killed it.
 
Also, timing regression tests are important when doing such reforms as
the above-mentioned string-literal reform, which has the potential to
severely slowdown the generated code.

--
  Peter



> 
> > ___
> > isabelle-dev mailing list
> > isabelle-...@in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 31/01/2019 20:37, Mathias Fleury wrote:
> 
>> On 31. Jan 2019, at 20:10, Makarius >
>> Can you point to these special applications?
>>
>> If export_code uses Generated_Files.add_files (in addition to
>> Export.export) we get both a check for unique names and an easy way to
>> retrieve the exports in Isabelle/ML, e.g. to write to a temporary
>> directory and do some tests.
> 
> Can you give some more details on how to achieve this?
> 
> Concrete application: I have a verified SAT solver (lets call that
> function isasat), an unverified parser, and several large CNF files
> (each one is several MB large). I would like to compile the SAT solver
> with MLton*, test it on those CNF files. With some timings information
> to identify regression if possible.
> 
>> So far I have never seen an application that could not be made stateless
>> and thus fit properly into the PIDE model.

The general principle is to keep generated material inside the theory
context (Generated_Files) and take them from there to produce other
artifacts in Isabelle/ML, e.g. as a "sink" to produce error information,
timing etc.

It is also possible to formally export sources or artifacts to the
session build database using Export.export: Isabelle/Scala can take
results from there and do something else with it, but inside the build
process, only after it.


* Here is a simple example with 'generated_file':


https://isabelle.in.tum.de/repos/isabelle/file/7e4966eaf781/src/Tools/Haskell/Haskell.thy

* Here is a test build inside Isabelle/ML -- this is stateless thanks to
a temp dir:


https://isabelle.in.tum.de/repos/isabelle/file/7e4966eaf781/src/Tools/Haskell/Test.thy

* Here is the use of the same sources in session database exports,
written to a global file-space that is not the Isabelle (or AFP) repository:


https://github.com/Naproche/Naproche-SAD/commit/698527fc6a47839bd48c521beb3d71129e3924a4


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Mathias Fleury]

Hi Makarius,

> On 31. Jan 2019, at 20:10, Makarius  wrote:
> 
> On 31/01/2019 18:27, Peter Lammich wrote:
>> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
>>> I have looked around at typical uses of 'export_code' in AFP. Most of
>>> the time it is just informative: writing a file and looking at it in
>>> the
>>> editor (or via the command-line!?), or doing that on the output
>>> channel.
>>> The isabelle-export: file-system covers that already, i.e. we should
>>> be
>>> able to eliminate almost all generated files from the AFP repository.
>>> 
>>> So "export_code .. file" should just disappear -- it is semantically
>>> illtyped in PIDE: editing the "file" argument will leave a trace of
>>> machine oil spilled to the physical file-system.
>> 
>> The problem here is actually deeper: 
>> Many AFP-entries are designed to export code which then works together
>> with some external code. However, there seems to be no way to test
>> whether this external code works with the generated code. 
> 
> Can you point to these special applications?
> 
> If export_code uses Generated_Files.add_files (in addition to
> Export.export) we get both a check for unique names and an easy way to
> retrieve the exports in Isabelle/ML, e.g. to write to a temporary
> directory and do some tests.

Can you give some more details on how to achieve this?

Concrete application: I have a verified SAT solver (lets call that function 
isasat), an unverified parser, and several large CNF files (each one is several 
MB large). I would like to compile the SAT solver with MLton*, test it on those 
CNF files. With some timings information to identify regression if possible.


> So far I have never seen an application that could not be made stateless
> and thus fit properly into the PIDE model.


Mathias


* Last time I tried, MLton was an order of magnitude faster than Poly/ML. But I 
can rewrite the parser for Poly/ML.

> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 31/01/2019 18:27, Peter Lammich wrote:
> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
>> I have looked around at typical uses of 'export_code' in AFP. Most of
>> the time it is just informative: writing a file and looking at it in
>> the
>> editor (or via the command-line!?), or doing that on the output
>> channel.
>> The isabelle-export: file-system covers that already, i.e. we should
>> be
>> able to eliminate almost all generated files from the AFP repository.
>>
>> So "export_code .. file" should just disappear -- it is semantically
>> illtyped in PIDE: editing the "file" argument will leave a trace of
>> machine oil spilled to the physical file-system.
> 
> The problem here is actually deeper: 
> Many AFP-entries are designed to export code which then works together
> with some external code. However, there seems to be no way to test
> whether this external code works with the generated code. 

Can you point to these special applications?

If export_code uses Generated_Files.add_files (in addition to
Export.export) we get both a check for unique names and an easy way to
retrieve the exports in Isabelle/ML, e.g. to write to a temporary
directory and do some tests.

So far I have never seen an application that could not be made stateless
and thus fit properly into the PIDE model.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Peter Lammich]

On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
> I have looked around at typical uses of 'export_code' in AFP. Most of
> the time it is just informative: writing a file and looking at it in
> the
> editor (or via the command-line!?), or doing that on the output
> channel.
> The isabelle-export: file-system covers that already, i.e. we should
> be
> able to eliminate almost all generated files from the AFP repository.
> 
> So "export_code .. file" should just disappear -- it is semantically
> illtyped in PIDE: editing the "file" argument will leave a trace of
> machine oil spilled to the physical file-system.

The problem here is actually deeper: 
Many AFP-entries are designed to export code which then works together
with some external code. However, there seems to be no way to test
whether this external code works with the generated code. 

There is the "checking"-option, which will test the generated code in
isolation. But any external code that is supposed to interface with the
generated code is left to bit-rotting.

--
  Peter

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 14/01/2019 20:20, Florian Haftmann wrote:
> 
>>   * Are there remaining uses of 'file' with empty name? Is the virtual
>> file-system browser sufficiently convenient to inspect results
>> interactively?
> 
> I checked the file system browser and would be quite content with it; as
> a bonus you can then make use of the syntax highlighting of jEdit (OCaml
> seems not be built-in, though).
> 
> But I want to excite more feedback of users.

Here is some feedback from myself as a user: the new stateless model to
generate files works well, in particular the file-browser of
Isabelle/jEdit helps.

There was only a technical problem it that should no longer occur in
practice, see

changeset:   69696:9fd395ff57bc
user:wenzelm
date:Sun Jan 20 21:26:15 2019 +0100
files:   Admin/components/components.sha1 Admin/components/main
src/Tools/jEdit/patches/vfs_manager
description:
avoid crash of jEdit.closeBuffer() via
TaskManager.instance.waitForIoTasks() due to race condition of save()
vs. automatic load() of already open buffer, e.g. relevant for save-as
on "isabelle-export:" artifacts;


In the mainstream this would probably be called a "fix", but the
conceptual problem behind it is still there: there are concurrent tasks
that are just concatenated in sequence, without taking the nesting of
the program structure into account. Proper futures are required instead
of slightly odd wait operations.


>>   * How to specify proper (unique) export names: PIDE still lacks a
>> check for uniqueness of export names, but overwriting existing exports
>> is considered illegal. The 'file' allowed to produce separate names in
>> the past, but it has a different meaning now (and is a candidate for
>> deletion).
> 
> Well, if we re-consider the syntax, we will also find a way for this.
> 
>> Maybe 'export_code' should be renovated replaced by reformed commands
>> like this:
>>
>>   * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is
>> optional and the default something like "generated" or "code". This
>> could be a "thy_decl" command that updates the theory context by
>> generated files that are accessible in Isabelle/ML, in addition to the
>> export; it would also include a check for duplicate names.
>>
>>   * "code_checking CONSTS in LANGUAGE" -- observing that "export_code
>> ... checking" is actually a different command. It would be a "diag"
>> command as before (this is relevant for parallelism).
> 
> Maybe the »checking« should just be a variant of the regular export.
> 
> Hence the modification could be quite conservative:
> 
>   export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
> ( file … | ( prefix … ) ( checked ) )
> 
> where »file« denotes a relative root in the file system and »checked«
> indicated that the generated code will be checked implicitly.

I have looked around at typical uses of 'export_code' in AFP. Most of
the time it is just informative: writing a file and looking at it in the
editor (or via the command-line!?), or doing that on the output channel.
The isabelle-export: file-system covers that already, i.e. we should be
able to eliminate almost all generated files from the AFP repository.

So "export_code .. file" should just disappear -- it is semantically
illtyped in PIDE: editing the "file" argument will leave a trace of
machine oil spilled to the physical file-system.


We do need an explicit prefix and an internal check for duplicates, e.g.
as in the command 'generated_file'.

That should be really just a prefix for the exported artifact, not the
name itself: each language processor should be smart enough to derive
file or directory names from it as required.  Thus the prefix locally
belongs in front of the arguments.

Here is an example from AFP/160ac13cdc05
SATSolverVerification/SatSolverCode.thy:

  export_code solve
in OCaml file "code/solve.ML"
in SML file "code/solve.ocaml
in Haskell file "code/"

It could be turned into something like this:

  export_code "code/" = solve in OCaml SML Haskell

Some details about the automatic name derivation scheme still need to be
sorted out -- or 'file' remains as an option to specify the suffix for
effective name (without writing anything to the file-system).


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Florian Haftmann]

Hi Makarius,

>   * Are there remaining uses of 'file' with empty name? Is the virtual
> file-system browser sufficiently convenient to inspect results
> interactively?

I checked the file system browser and would be quite content with it; as
a bonus you can then make use of the syntax highlighting of jEdit (OCaml
seems not be built-in, though).

But I want to excite more feedback of users.

>   * How to specify proper (unique) export names: PIDE still lacks a
> check for uniqueness of export names, but overwriting existing exports
> is considered illegal. The 'file' allowed to produce separate names in
> the past, but it has a different meaning now (and is a candidate for
> deletion).

Well, if we re-consider the syntax, we will also find a way for this.

> Maybe 'export_code' should be renovated replaced by reformed commands
> like this:
> 
>   * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is
> optional and the default something like "generated" or "code". This
> could be a "thy_decl" command that updates the theory context by
> generated files that are accessible in Isabelle/ML, in addition to the
> export; it would also include a check for duplicate names.
> 
>   * "code_checking CONSTS in LANGUAGE" -- observing that "export_code
> ... checking" is actually a different command. It would be a "diag"
> command as before (this is relevant for parallelism).

Maybe the »checking« should just be a variant of the regular export.

Hence the modification could be quite conservative:

export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
( file … | ( prefix … ) ( checked ) )

where »file« denotes a relative root in the file system and »checked«
indicated that the generated code will be checked implicitly.

So far my current thoughts.

Florian



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 11/01/2019 11:51, Makarius wrote:
> On 10/01/2019 16:38, Makarius wrote:
>> On 10/01/2019 16:28, Florian Haftmann wrote:
>>> Code generation: command 'export_code' without file keyword exports
>>> code as regular theory export, which can be materialized using tool
>>> 'isabelle export'; to get generated code dumped into output, use
>>> 'file ""'.  Minor INCOMPATIBILITY.
>>>
>>> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc
>>> generated code in AFP-entries.
>>
>> Great, I will try this out soon.
> 
> I have started looking and thinking about it again.

I have reworked this a bit in Isabelle/e61b0b819d28: Isabelle/jEdit is
able to browse theory exports via the virtual file-system
"isabelle-export:" and the 'export_code' command emits some information
message about it.

There are still a few open questions:

  * Are there remaining uses of 'file' with empty name? Is the virtual
file-system browser sufficiently convenient to inspect results
interactively?

  * How to specify proper (unique) export names: PIDE still lacks a
check for uniqueness of export names, but overwriting existing exports
is considered illegal. The 'file' allowed to produce separate names in
the past, but it has a different meaning now (and is a candidate for
deletion).


Maybe 'export_code' should be renovated replaced by reformed commands
like this:

  * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is
optional and the default something like "generated" or "code". This
could be a "thy_decl" command that updates the theory context by
generated files that are accessible in Isabelle/ML, in addition to the
export; it would also include a check for duplicate names.

  * "code_checking CONSTS in LANGUAGE" -- observing that "export_code
... checking" is actually a different command. It would be a "diag"
command as before (this is relevant for parallelism).


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 10/01/2019 16:38, Makarius wrote:
> On 10/01/2019 16:28, Florian Haftmann wrote:
>> Code generation: command 'export_code' without file keyword exports
>> code as regular theory export, which can be materialized using tool
>> 'isabelle export'; to get generated code dumped into output, use
>> 'file ""'.  Minor INCOMPATIBILITY.
>>
>> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc
>> generated code in AFP-entries.
> 
> Great, I will try this out soon.

I have started looking and thinking about it again.

First note that Export.export_raw is only required for very big exports
that have their own compression somehow built in. You can always use
Export.export in regular applications: the compression status is stored
in the database, and the exported result is uncompressed.


> I've had some discussions with users of Haskell code generation, e.g.
> AFP/HLDE.
> 
> My conclusions so far:
> 
>   * primary (default) output should be via the new Generated_Files
> module in Isabelle/ML; thus applications can refer to file content via a
> theory context, e.g. to write it to the file-system via
> Generated_Files.write_files.
> 
>   * secondary output works via the Export interface to Isabelle/Scala;
> e.g. I could easily add Generated_Files.export_files for that and
> export_code would merely use Generated_Files.add_files (no export yet).

I have added Generated_Files.export_files in Isabelle/a2fbfdc5e62d: the
generated sources from Isabelle/Haskell serve as an example.


How to proceed from here is still unclear. I will look more closely at
the applications of 'export_code' in AFP. The question is if we can get
rid of all options for experimentation ('file') and have the Prover IDE
and system environment take care of it.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Makarius]

On 10/01/2019 16:28, Florian Haftmann wrote:
> Code generation: command 'export_code' without file keyword exports
> code as regular theory export, which can be materialized using tool
> 'isabelle export'; to get generated code dumped into output, use
> 'file ""'.  Minor INCOMPATIBILITY.
> 
> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc
> generated code in AFP-entries.

Great, I will try this out soon.

On Mon..Wed this week I visited the Innsbruck Isabelle site (the city of
Innsbruck is very professional in managing a lot of snow without
hindering public life :-)

I've had some discussions with users of Haskell code generation, e.g.
AFP/HLDE.

My conclusions so far:

  * primary (default) output should be via the new Generated_Files
module in Isabelle/ML; thus applications can refer to file content via a
theory context, e.g. to write it to the file-system via
Generated_Files.write_files.

  * secondary output works via the Export interface to Isabelle/Scala;
e.g. I could easily add Generated_Files.export_files for that and
export_code would merely use Generated_Files.add_files (no export yet).


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev