Re: [isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources

[Makarius]

On 31/01/2019 23:11, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
> 
> * The jEdit File Browser is more prominent in the default GUI layout of
> Isabelle/jEdit: various virtual file-systems provide access to Isabelle
> resources, notably via "favorites:" (or "Edit Favorites").

There is an old oddity in "Edit Favorites" that I have now addressed here:

changeset:   69779:a2218981a5d6
user:wenzelm
date:Thu Jan 31 22:02:50 2019 +0100
files:   src/Tools/jEdit/patches/favorites
description:
more accurate _listFiles -- avoid infinite infinite expansion of e.g.
"$ISABELLE_HOME";


This minor change is not yet active: a future update of the jedit_build
component will include it.


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

[isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources

[Makarius]

*** Isabelle/jEdit Prover IDE ***

* The jEdit File Browser is more prominent in the default GUI layout of
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
resources, notably via "favorites:" (or "Edit Favorites").

* Action "isabelle-export-browser" points the File Browser to the theory
exports of the current buffer, based on the "isabelle-export:" virtual
file-system. The directory view needs to be reloaded manually to follow
ongoing document processing.

* Action "isabelle-session-browser" points the File Browser to session
information, based on the "isabelle-session:" virtual file-system. Its
entries are structured according to chapter / session names, the open
operation is redirected to the session ROOT file.


This refers to Isabelle/b9a5805d1d70. I have also change the default GUI
layout: global overview LEFT (Documentation, File Browser), local
document information RIGHT (Theories, SideKick etc.) Output and
interaction at the BOTTOM, as before.

Within the repository I cannot impose arbitrary jEdit properties on a
local settings directory, so it might require manual tinkering to
imitate the default. (I usually rename $ISABELLE_HOME_USER/jedit
temporarily to see the difference.)


The "isabelle-session:" virtual file-system is the start of more serious
access to Isabelle resources: right now it merely shows chapter/session
tree structure, and opens the corresponding ROOT entry. Since the latter
is also under PIDE control, CTRL/COMMAND-MOUSE-HOVER-CLICK quickly leads
to some theories.


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

[isabelle-dev] NEWS: option "jedit_text_overview"

[Makarius]

*** Isabelle/jEdit Prover IDE ***

* System option "jedit_text_overview" allows to disable the text
overview column.


This refers to Isabelle/5a8ae7a4b7d0 -- it is a minor visual enhancement
for situations where the editor screen should look like a presentation,
without any distractions by extra GUI elements. (All other GUI elements
had already options in jEdit or Isabelle).


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 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] Afterthoughts on Local_Theory.subtarget_result

[Makarius]

On 22/01/2019 22:24, Florian Haftmann wrote:
> 
> as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
> seen Local_Theory.reset invocations are gone, conveniently replaced by
> Local_Theory.subtarget_result.

This looks clean and canonical. At least we have Local_Theory.reset out
of the way in visible Isabelle/ML tool implementations: it is still
present inside Local_Theory.close_target, though.

I wonder what happens when that is removed: presumably it requires a lot
of fine-tuning to make everything work again without that hidden reset.


Makarius



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