Re: [isabelle-dev] AFP/HLDE

[Makarius]

On 10.10.2018 20:51, Florian Haftmann wrote:

Can 'export_code' do that, with a slight modification to produce formal
exports via Export.export?


That what indeed be feasible.

Instead of "file", a keyword like "prefix" could be given to "export_code".


As long as 'prefix' is not an actual keyword of outer syntax: it is 
likely to be a plain name somewhere.


Some tools use Parse.reserved instead of keyword as a workaround.


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

Re: [isabelle-dev] AFP/HLDE

[Florian Haftmann]

> Can 'export_code' do that, with a slight modification to produce formal
> exports via Export.export?

That what indeed be feasible.

Instead of "file", a keyword like "prefix" could be given to "export_code".

I will put this into my pipeline to implement, but it will take some
time until this will take shape, the code generator printing layers are
very technical.

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] AFP/HLDE

[Makarius]

On 09/10/18 10:57, Christian Sternagel wrote:
> On 10/08/2018 04:14 PM, Makarius wrote:
>> On 08/10/18 15:58, Lars Hupel wrote:
>>
>> I don't mind if it is possible to eliminate AFP/HLDE (theory
>> Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from
>> doing such things in AFP.
>>
> 
> Compiling a binary in HLDE was a mere experiment on our side too. So I
> also do not mind much to remove this again from the AFP.
> 
> I would however like to keep theory Solver_Code and still let it
> generate Haskell source code (that is required for the handwritten Main.hs).

The still open question is how to generate the Haskell source without
writing into odd place of the file-system.

Can 'export_code' do that, with a slight modification to produce formal
exports via Export.export?


Makarius

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

Re: [isabelle-dev] AFP/HLDE

[Christian Sternagel]

On 10/08/2018 04:14 PM, Makarius wrote:
> On 08/10/18 15:58, Lars Hupel wrote:
> 
> I don't mind if it is possible to eliminate AFP/HLDE (theory
> Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from
> doing such things in AFP.
> 

Compiling a binary in HLDE was a mere experiment on our side too. So I
also do not mind much to remove this again from the AFP.

I would however like to keep theory Solver_Code and still let it
generate Haskell source code (that is required for the handwritten Main.hs).

Then the task of setting up a proper Haskell environment and compiling
an executable is moved to prospective users. Which is fine with me.

cheers

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

Re: [isabelle-dev] AFP/HLDE

[Makarius]

On 08/10/18 15:58, Lars Hupel wrote:
>> For the ROOT entry there is already 'export_files' in Isabelle2018. This
>> could be augmented by something like:
>>
>>   export_action NAME = SCALA
>>
>> with a snippet of Scala source that is a function from the resulting
>> session build to unit. It could invoke build tools for Haskell, Ocaml,
>> Scala, SML, even LaTeX in Isabelle/Scala.
> 
> Let's call this facility "build actions" for simplicity.

I've called it export_action, because it happens outside the regular
build, based on static data in the session database.

Another application of it (with different user interface) would be
document preparation: the session exports .tex files the database, some
export action produces .pdf files with pdflatex later on.


> The question about build actions is: do they solve the problem in the
> AFP, e.g. with HLDE? Invoking arbitrary build tools (i.e. running
> arbitrary code) is a problem for two reasons:

The current problem are files written in odd places as a side-effect of
the session build.

There is already the possibility to invoke strange things via
Isabelle_System.bash inside Isabelle/ML.


> Again – hypothetically – assume that Peter submits this to the AFP,
> using build actions. He'd write something like:
> 
>   export_action tool =
> Isabelle_System.bash("cmake . && make && make install")
> 
> This is going to be a nightmare. There's virtually nothing you can
> assume about the C/C++ toolchain that's present on any given system. In
> Haskell/Scala/OCaml one can at least install packages without root
> privileges, but not in C.

We need to be indeed vary of not having the evil C/C++ tool chain come
back on us. We actually do have such tendencies right now, with the
cakeml setup and also opam (it uses "make" internally).


> To summarize: The above is, at best, a weak argument against build
> actions in general. But I think it is a strong argument against build
> actions in the AFP.

I don't mind if it is possible to eliminate AFP/HLDE (theory
Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from
doing such things in AFP.

There is already "isabelle export" to export plain data, without running
anything. But then I foresee funny Makefiles showing up in AFP based on
"isabelle build" and "isabelle export" plus a shell action to run other
tools on the result.


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

Re: [isabelle-dev] AFP/HLDE

[Lars Hupel]

> For the ROOT entry there is already 'export_files' in Isabelle2018. This
> could be augmented by something like:
> 
>   export_action NAME = SCALA
> 
> with a snippet of Scala source that is a function from the resulting
> session build to unit. It could invoke build tools for Haskell, Ocaml,
> Scala, SML, even LaTeX in Isabelle/Scala.

Let's call this facility "build actions" for simplicity.

The current approach of "export_code ... checking" is, in my opinion, a
sweet spot. It can be kept working with modest effort. It doesn't test a
whole lot of things though. Making opam and stack available will help us
in the medium term by abstracting exactly what is needed for raw code
generation away from distributions.

The question about build actions is: do they solve the problem in the
AFP, e.g. with HLDE? Invoking arbitrary build tools (i.e. running
arbitrary code) is a problem for two reasons:

– A consistent environment where everything that's needed for any given
application is very hard to guarantee. The closest technologies we have
for that are currently Nix and Docker. (It's no coincidence that Nix
uses "closure" terminology.)

– What are the maintenance guarantees? If something breaks in the
generated code, violating assumptions from third-party code, who will
fix it?

As a case study, consider the "Iptables_Semantics" entry. It produces
non-trivial amounts of code that is subsequently decorated with
hand-written Haskell code that requires ~5 third-party packages.
Currently, all of this is kept in a separate repository. Assume for a
moment that this were to move into the AFP. Now, also assume evolution
of the Isabelle system (for example, some code printing). Things will
break. Furthermore, without additional efforts, this can't just build on
arbitrary machines (not even Stack fixes that fully).

But it gets worse. Let's consider another case study. Peter's GRAT
checker is currently only available in the IsaFoL repository:
. This project
consists of an Isabelle part and a C part. The latter is built with CMake.

Again – hypothetically – assume that Peter submits this to the AFP,
using build actions. He'd write something like:

  export_action tool =
Isabelle_System.bash("cmake . && make && make install")

This is going to be a nightmare. There's virtually nothing you can
assume about the C/C++ toolchain that's present on any given system. In
Haskell/Scala/OCaml one can at least install packages without root
privileges, but not in C.

Docker could fix that. But then we're back at the ever-looming question
of maintenance.

To summarize: The above is, at best, a weak argument against build
actions in general. But I think it is a strong argument against build
actions in the AFP.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP/HLDE

[Christian Sternagel]

On 10/05/2018 10:14 PM, Makarius wrote:
> 
> So the question is reduced by one step: What is the purpose of theory
> "Solver_Code" abstractly?

I just wanted to confirm that the purpose of Solve_Code is to produce a
Haskell executable (that implements an algorithm that was formalized in
the AFP entry). Or as you put it yourself:

The abstract application I see here is: use Isabelle to produce some
executable in Haskell (or OCaml, or Scala, or SML).

cheers

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

Re: [isabelle-dev] AFP/HLDE

[Makarius]

On 06/10/18 13:22, Florian Haftmann wrote:
> 
> a) Plain code generation to the file system (export_code … in … …); the
> most basic use case.

Could we have an alternative to the file/directory interface for formal
exports just now? The main operation is Export.export with a structured
name (separated by slashes) and arbitrary content (bytes). This
replaces Isabelle_System.mkdirs / File.write operations.

The exported results could be accessed later by other tools outside the
session context.


> What we have in $AFP/Diophantine_Eqns_Lin_Hom/Solver_Code.thy is
> another, not-yet well integrated issue:
> 
> e) Using generated code in bigger integrative processes to derive build
> results from it.  Also some kind of generalization of c).
> 
> There is indeed need for more »cultivation«, but IMHO we should resist
> the temptation to put more and more programming language environment
> interfaces into Isabelle: that would lead to mimic their divergent and
> sophisticated concepts inside our environment (the reason why c) is
> comparably simple to achieve is that out of 4 implemented target
> languages Scala and SML are already well-integrated into Isabelle).

The abstract application I see here is: use Isabelle to produce some
executable in Haskell (or OCaml, or Scala, or SML).

Thus it is related to other open questions about setting up a
well-defined project build environment for these languages. Scala and
SML are already somehow special to Isabelle, so it is mainly about
Haskell and OCaml.

After looking around very briefly, I would continue with the hypothesis
that Haskell "stack" and OCaml "opam" could do this for use: provide one
and only one well-defined version, independently of the underlying OS
distribution. (But having "stack" and "opam" around would still allow
users to do other things with them, like playing around with many
different versions and packages.)


> What about the other way round, i.e. integrating Isabelle into specific
> programming language environments? It could work roughtly as follows:
> * Generated code is a resource that can be exported from a session.
> * Hence arbitrary programming language environment can use Isabelle to
> obtain generated code.
> * Its integration and compilation than happens just by existing tools of
> that programming language environment, without burdening Isabelle at all.
> * We would still need a way to integrate such constructs into our build
> and session system, to express such things as »run this session, take
> those results, put them into that programm call, expect the following
> result and continue with …«; but this can maybe done by having a
> construct in ROOT files which does not denote a regular theory session
> but a operational logic implemented by a piece of Scala running in a
> dedicated environment.

I think we need a well-balanced construction that addresses our typical
requirements, without imposing 16 tons weight on the platform without a
real purpose (that would happen by default without looking very carefully).

Presently, I am thinking in terms of Isabelle tools like "haskell_setup"
and "ocaml_setup", with "stack" and "opam" at the bottom. These would
provide ISABELLE_HASKELL and ISABELLE_OCAML settings.


For the ROOT entry there is already 'export_files' in Isabelle2018. This
could be augmented by something like:

  export_action NAME = SCALA

with a snippet of Scala source that is a function from the resulting
session build to unit. It could invoke build tools for Haskell, Ocaml,
Scala, SML, even LaTeX in Isabelle/Scala.

That would be clearly outside of the session context of the Isabelle/ML
process: no funny shell scripts in ML, no odd files written to the
source file-system (nor ISABELLE_TMP, nor ISABELLE_HOME_USER).


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

Re: [isabelle-dev] AFP/HLDE

[Florian Haftmann]

Dear all,

> It seems to deliver an executable tool for later use elsewhere, but the
> implementation is very fragile.
> 
> We could take it as a model to get such a task right.

the situation wrt. generated code is indeed somehow baroque.

I am aware of the following layers / approaches:

a) Plain code generation to the file system (export_code … in … …); the
most basic use case.

b) Integration of code generation with the Isabelle/ML runtime; this
refers to evaluation and computations, and has reached a quite
satisfactory state.

c) Simple ad-hoc compilation checks (export_code … checking …) as
./src/HOL/Codegenerator_Test; this has always been mere device to check
that nothing utterly wrong has happended to the code generator.

d) Evaluation beyond Isabelle/ML (in src/HOL/Library/Code_Test.thy);
some kind of generalization of c).

What we have in $AFP/Diophantine_Eqns_Lin_Hom/Solver_Code.thy is
another, not-yet well integrated issue:

e) Using generated code in bigger integrative processes to derive build
results from it.  Also some kind of generalization of c).

There is indeed need for more »cultivation«, but IMHO we should resist
the temptation to put more and more programming language environment
interfaces into Isabelle: that would lead to mimic their divergent and
sophisticated concepts inside our environment (the reason why c) is
comparably simple to achieve is that out of 4 implemented target
languages Scala and SML are already well-integrated into Isabelle).

What about the other way round, i.e. integrating Isabelle into specific
programming language environments? It could work roughtly as follows:
* Generated code is a resource that can be exported from a session.
* Hence arbitrary programming language environment can use Isabelle to
obtain generated code.
* Its integration and compilation than happens just by existing tools of
that programming language environment, without burdening Isabelle at all.
* We would still need a way to integrate such constructs into our build
and session system, to express such things as »run this session, take
those results, put them into that programm call, expect the following
result and continue with …«; but this can maybe done by having a
construct in ROOT files which does not denote a regular theory session
but a operational logic implemented by a piece of Scala running in a
dedicated environment.

So far a few raw thoughts.

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] AFP/HLDE

[Makarius]

On 05/10/18 20:20, Christian Sternagel wrote:
> 
> On 10/05/2018 07:10 PM, Makarius wrote:
>> What is the purpose of the session HLDE, with its duplicate theory
>> Solver_Code that is also in Diophantine_Eqns_Lin_Hom?
> 
> As the author of the corresponding ROOT file, when I look at it now, I
> cannot think of any reason to have also session HLDE (except of course
> the shorter name).

So the question is reduced by one step: What is the purpose of theory
"Solver_Code" abstractly?

It seems to deliver an executable tool for later use elsewhere, but the
implementation is very fragile.

We could take it as a model to get such a task right.


Makarius

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

Re: [isabelle-dev] AFP/HLDE

[Christian Sternagel]

Dear Makarius

On 10/05/2018 07:10 PM, Makarius wrote:
> What is the purpose of the session HLDE, with its duplicate theory
> Solver_Code that is also in Diophantine_Eqns_Lin_Hom?

As the author of the corresponding ROOT file, when I look at it now, I
cannot think of any reason to have also session HLDE (except of course
the shorter name).

cheers

chris

> 
> I've had seen odd crashes due to its non-temporary output into
> ISABELLE_TMP, but the technical problem behind it might be actually in
> Isabelle/Scala (rm_tree):
> 
> Exception in thread "process_manager" java.nio.file.NoSuchFileException:
> /tmp/isabelle-mawenzel/process7653301744367976304/HLDE/Main.hi
> at
> sun.nio.fs.UnixException.translateToIOException(UnixException.java:86)
> 
> (Isabelle/742c88258cf8 + AFP/854bc290d72b + a derivative of "isabelle
> dump" that is not in these repositories).
> 
> 
> The HLDE session also touches the open question how to deal with
> generated material in AFP. We have already a concept for "exports" in
> Isabelle2018 (see NEWS). Maybe that is already sufficient that we can
> make such sessions pure in the sense that nothing is written into odd
> places in the file-system, only into the formal session database.
> 
> 
>   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