Re: [isabelle-dev] NEWS

[Makarius]

On 13/03/2019 21:12, Makarius wrote:
> On 13/03/2019 21:00, Florian Haftmann wrote:
>> Am 13.03.19 um 20:57 schrieb Lars Hupel:
   isabelle ocaml_opam install zarith
>>>
>>> This should ideally happen on-the-fly from within Isabelle/ML.
>>
>> Or maybe as implicit part  of
>>
>>  isabelle ocaml_setup
> 
> Note that any change of the physical environment needs to happen in
> administrative tools like "isabelle ocaml_setup": there is an implicit
> assumption that there is only one administrator doing one thing at a
> time. (E.g. in "isabelle build" and its physical update of heap and db
> files.)
> 
> In contrast, the parallel Isabelle/ML world cannot write to the global
> file-system, without causing big problems.

This requirement of statelessness also applies to the etc/settings shell
scripts in the Isabelle components hierarchy. We have recently had
tendencies to postulate automated build or download features here, but
this is not going to work. There can be many simultaneous invocations of
these scripts, and we cannot afford races, long-running operations, or
spurious failures.


Here is an example where I have amended such a mistake of mine,
concerning Haskell stack:
http://isabelle.in.tum.de/repos/isabelle/rev/c911716d29bb -- before
there were spurious "stack" operations to access its stackage repository
in uncontrolled ways.

I've forgotten to apply the analogous change to the Isabelle/Naproche
project (to be found on Github): it has already caused a lot of problems
just with 2 developers and 3 users trying it out at Uni Bonn.

I will have to revise "isabelle ghc_setup" further, to leave more
accurate information in its installation directory (about
platform-specific paths to ghc). Thus etc/settings can refer to that
robustly and portably (note that even just different Linux installations
may lead to different ghc installation names; of course it also needs to
work with Windows and macOS on the same shared stack installation).


Compared to that, "isabelle opam" is still lagging behing in various
respects. I have myself no experience with the underlying opam tool, and
it is also the old version 1.2.2 (which was imposed by Cygwin some
months ago).


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

Re: [isabelle-dev] NEWS

[Makarius]

On 13/03/2019 21:00, Florian Haftmann wrote:
> Am 13.03.19 um 20:57 schrieb Lars Hupel:
>>>   isabelle ocaml_opam install zarith
>>
>> This should ideally happen on-the-fly from within Isabelle/ML.
> 
> Or maybe as implicit part  of
> 
>   isabelle ocaml_setup

Note that any change of the physical environment needs to happen in
administrative tools like "isabelle ocaml_setup": there is an implicit
assumption that there is only one administrator doing one thing at a
time. (E.g. in "isabelle build" and its physical update of heap and db
files.)

In contrast, the parallel Isabelle/ML world cannot write to the global
file-system, without causing big problems. We have pending issues with
AFP entries that violate this principle: maybe we manage to put it all
into shape for the Isabelle2019 release, using stateless operations from
Export/Generated_Files in ML for the 'codegen' command in particular.


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

Re: [isabelle-dev] NEWS

[Lars Hupel]

Or maybe as implicit part  of

isabelle ocaml_setup


Sure, that could also work.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS

[Florian Haftmann]

Am 13.03.19 um 20:57 schrieb Lars Hupel:
>>   isabelle ocaml_opam install zarith
> 
> This should ideally happen on-the-fly from within Isabelle/ML.

Or maybe as implicit part  of

isabelle ocaml_setup

?

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

[Lars Hupel]

  isabelle ocaml_opam install zarith


This should ideally happen on-the-fly from within Isabelle/ML.

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

[isabelle-dev] NEWS: Update to Poly/ML 5.8 -- and towards Isabelle2019

[Makarius]

*** System ***

* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
applications compared to old x86 mode (which is no longer used by
Isabelle). The switch to the x86_64 CPU architecture also avoids
compatibility problems with Linux and macOS, where 32-bit applications
are gradually phased out.


This refers to Isabelle/63721ee8c86c, it is now the official release of
Poly/ML 5.8 by David Matthews.

It all looks great so far, and there is still plenty of time for further
testing until the official release of Isabelle2019.

The present plan is to publish an unofficial Isabelle2019-RC0 snapshot
in early April, and start officially with Isabelle2019-RC1 at the
beginning of May. It all should be finalized an published until
15-Jun-2019, when I will go on travel (not vacation, but a visit to
colleagues in Paris).


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

[isabelle-dev] NEWS: option system_heaps

[Makarius]

*** Isabelle/jEdit Prover IDE ***

* Command-line options "-s" and "-u" of "isabelle jedit" override the
default for system option "system_heaps" that determines the heap
storage directory for "isabelle build". Option "-n" is now clearly
separated from option "-s".


*** System ***

* The system option "system_heaps" determines where to store the session
image of "isabelle build" (and other tools using that internally).
Former option "-s" is superseded by option "-o system_heaps".
INCOMPATIBILITY in command-line syntax.


This refers to Isabelle/cc0b3e177b49.

Short version: "isabelle build -s" is now "isabelle build -o
system_heaps", and various other command-lines have been simplified. It
is also possible to provide system_heaps via etc/preferences.


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 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: 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").

I have now reverted the default to "buffer" instead of "favorites", see

changeset:   69781:a7529ac9c1c5
user:wenzelm
date:Fri Feb 01 15:02:36 2019 +0100
files:   src/Tools/jEdit/src/jEdit.props
description:
clarified default (amending ca9780325a21): it also affects "open-file"
dialog, which should be "buffer";


The favorites are very important, but many long-term users still don't
know about them. I need to find another way to make them easily accessible.


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

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

[Florian Haftmann]

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.

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

[isabelle-dev] NEWS: isabelle update

[Makarius]

*** System ***

* The command-line tool "isabelle update" uses Isabelle/PIDE in
batch-mode to update theory sources based on semantic markup produced in
Isabelle/ML. Actual updates depend on system options that may be enabled
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
section "Theory update". Theory sessions are specified as in "isabelle
dump".


This refers to Isabelle/1d2d4ae9ab81 and there is some documentation in
the "system" manual as usual. The "isabelle update" tool is a corollary
of the "Headless PIDE" session; it opens new possibilities for
systematic maintenance of formal sources at a large scale. In the next
round I will provide options to replace old-style ASCII syntax, e.g. %
== ==> -->.

An example is Isabelle/a96320074298, which is the result of applying
"isabelle update -u path_cartouches" for all sessions.


So far I have refrained from too much updating, because I am not sure
how far we are in the process of mental adaption, to see cartouches
almost everywhere. In particular "isabelle update -u
inner_syntax_cartouches" will be quite significant:

  * Different visual appearance of Isabelle sources: potentially odd for
long-term users, but less odd for newcomers (i.e. no longer questions
like "What is the meaning of double-quotes around the logical language?"
at first-time exposure).

  * It potentially affects corner cases for implicit or explicit
double-quotes in document preparation (cf. options thy_output_quotes /
thy_output_source or @{term [quotes] "..."} / @{term [source] "..."}).

  * When inner syntax double-quotes are discontinued eventually, the
inner syntax of the HOL library may use double quotes for char/string
literals, instead of slightly odd double single-quotes.


Here is a reminder of the general approach and trend of recent years:

  * embedded languages normally use cartouches, while double quotes are
old-style / legacy;

  * names normally use plain identifiers, but double quotes are
available to escape conflicts with keywords.


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

Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts

[Makarius]

On 24/11/2018 19:51, Makarius wrote:
> 
> *** Isabelle/jEdit Prover IDE ***
> 
> * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
> DejaVu" collection by default, which provides uniform rendering quality
> with the usual Isabelle symbols. For Java/Swing GUI elements this
> requires the Metal look-and-feel: it is the default on Linux, but not
> macOS nor Windows. Line spacing no longer needs to be adjusted:
> properties for the old IsabelleText font had "Global Options / Text Area
> / Extra vertical line spacing (in pixels): -2", now it defaults to 0.

I have reworked this further in various changesets leading up to
Isabelle/429426640596. In particular, the Isabelle fonts are now forced
on all Java/Swing look-and-feels, by modifying some UIManager font
properties.

This appears to work reasonably well on Linux GTK+, Windows, Mac OS X,
but we need to keep an eye on it for fine points and drop-outs. (For
Metal look-and-feel and already worked uniformly before.)

The idea is that GUI elements use "Isabelle DejaVu Sans" (not "Mono")
wherever feasible. Thus all mathematical symbols and special  icons
should be always correctly displayed (e.g. in Hypersearch tree view).
The regular search dialog now also uses this font: before it was the
main text area font (usually the "Mono" version).


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

Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts

[Makarius]

On 24/11/2018 19:51, Makarius wrote:
> *** General ***
> 
> * The font family "Isabelle DejaVu" is systematically derived from the
> existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
> and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
> The DejaVu base fonts are retricted to well-defined Unicode ranges and
> augmented by special Isabelle symbols, taken from the former
> "IsabelleText" font (which is no longer provided separately).

Side-remark: this works via "isabelle build_fonts -d
dejavu-fonts-ttf-2.37/ttf"

The Isabelle/Scala sources of this tool should be obvious, see
http://isabelle.in.tum.de/repos/isabelle/file/395c4fb15ea2/src/Pure/Admin/build_fonts.scala


In the past, people have occasionally pointed out that the standard
Isabelle font is a bit boring. If there are other high-quality fonts to
be considered for the Isabelle font portfolio, I am interested to hear
about them.

Of course, it is also possible to use private Isabelle-derivatives of
existing fonts, such as some Apple fonts that are provided with macOS.
(These are usually non-free and we cannot ship them by default.)

It is generally better to have all special glyphs in a single font where
all sizes are carefully fit together, instead of implicit or explicit
multi-font assembly in GUI frameworks.


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

[isabelle-dev] NEWS: Isabelle DejaVu fonts

[Makarius]

*** General ***

* The font family "Isabelle DejaVu" is systematically derived from the
existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
The DejaVu base fonts are retricted to well-defined Unicode ranges and
augmented by special Isabelle symbols, taken from the former
"IsabelleText" font (which is no longer provided separately). The line
metrics and overall rendering quality is closer to original DejaVu.
INCOMPATIBILITY with display configuration expecting the old
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.


* The Isabelle fonts render "¯" properly as superscript "-1".

*** Isabelle/jEdit Prover IDE ***

* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
DejaVu" collection by default, which provides uniform rendering quality
with the usual Isabelle symbols. For Java/Swing GUI elements this
requires the Metal look-and-feel: it is the default on Linux, but not
macOS nor Windows. Line spacing no longer needs to be adjusted:
properties for the old IsabelleText font had "Global Options / Text Area
/ Extra vertical line spacing (in pixels): -2", now it defaults to 0.

* Improved sub-pixel font rendering (especially on Linux), thanks to
OpenJDK 11.


This refers to Isabelle/395c4fb15ea2 and Isabelle/6aa24ccd8049.

The idea to construct Isabelle fonts systematically with the fontforge
scripting language has been in the pipeline for a long time. It has now
been flushed due to the change of font-rendering in the OpenJDK 11
version that we are using: now we have proper bold-italic fonts as well,
which is relevant to render control symbols like \<^term>.

I have taken the opportunity to brush-up the whole font setup, such that
we are again a little better of than before, according to the strict
monotonicity principle of Isabelle development.


Users hooked on isabelle-dev versions might have to revisit their
Isabelle/jEdit properties, to ensure that no "IsabelleText" font
specifications are left. Already existing user properties take
precedence over defaults provided by Isabelle/jEdit: see
$ISABELLE_HOME_USER/jedit/properties vs.
$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props and recall that the
"properties" file cannot be changed while Isabelle/jEdit is running (it
will be overwritten on application shutdown).


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

Re: [isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala

[Makarius]

On 11/11/2018 16:44, Lars Hupel wrote:
>> * Support for Isabelle command-line tools defined in Isabelle/Scala.
>> Instances of class Isabelle_Scala_Tools may be configured via the shell
>> function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
>> component).
> 
> This is nice! Anything on the radar to automate compilation as well,
> just like `jedit -bf`, but for arbitrary components? That would be very
> useful for the AFP.

I know, and I've (re)started thinking about it.

Somehow there should be a mechanism to augment the Admin/build process
in user-space. It would also mean to get rid of the special "isabelle
jedit -b" in various situations of system initialization.


Makarius


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

Re: [isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala

[Lars Hupel]

* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).


This is nice! Anything on the radar to automate compilation as well, 
just like `jedit -bf`, but for arbitrary components? That would be very 
useful for the AFP.

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

[isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala

[Makarius]

*** System ***

* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).


This refers to Isabelle/258bef08b31e. In recent years we have seen a
trend to use proper Isabelle/Scala instead of odd scripts (Bash, Perl,
Python etc.). Now it is possible to do this for user-space components
that provide their own classpath jars with instances of class
Isabelle_Scala_Tools. So far this only worked for .scala scripts, which
where interpreted.


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

Re: [isabelle-dev] NEWS: support for GHC

[Makarius]

This is the updated situation according to Isabelle/c1a27fce2076:


*** System ***

* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:

  isabelle ghc_setup
  isabelle ghc_stack

  isabelle ocaml_setup
  isabelle ocaml_opam

The global installation state is determined by the following settings
(and corresponding directory contents):

  ISABELLE_STACK_ROOT
  ISABELLE_STACK_RESOLVER
  ISABELLE_GHC_VERSION

  ISABELLE_OPAM_ROOT
  ISABELLE_OCAML_VERSION

After setup, the following Isabelle settings are automatically
redirected (overriding existing user settings):

 ISABELLE_GHC

 ISABELLE_OCAML
 ISABELLE_OCAMLC

The old meaning of these settings as locally installed executables may
be recovered by purging the directories ISABELLE_STACK_ROOT /
ISABELLE_OPAM_ROOT.



I have also started experimenting with the following in
$ISABELLE_HOME_USER/etc/settings:

  ISABELLE_STACK_ROOT="$HOME/.stack"
  ISABELLE_OPAM_ROOT="$HOME/.opam"

The Isabelle scripts should ensure that the specified versions are used,
independently of other versions that a user might have installed already.

In any case, both "stack" and "opam" stack-up considerable material: it
is easy to fill 5-15 GB of disk space after working some time. Only
docker requires even more space.


Makarius

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

Re: [isabelle-dev] NEWS: support for GHC

[Bertram Felgenhauer]

Makarius wrote:
> On 08/11/2018 14:59, Bertram Felgenhauer wrote:
> >>
> >> I've misunderstood the problem. You intend to invoke old-style
> >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> > 
> > This may be premature, but I foresee that now that `isabelle ghc`
> > and `isabelle ghci` exist, we will have scripts that use them.
> 
> There is indeed some confusion here.
> 
> My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained
> by the odd recursive setup: in the stack situation, $ISABELLE_GHC points
> to lib/Tools/ghc, and some mistake in the configuration could lead to
> infinite recursion of sub-processes (potential bombing of the OS).
> 
> It is probably better to leave the meaning of ISABELLE_GHC (and
> ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle
> ghc" tool entry points: these auxiliary scripts should go into
> $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular
> Isabelle tools.

Sounds good to me.

Cheers,

Bertram

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

Re: [isabelle-dev] NEWS: support for GHC

[Makarius]

On 08/11/2018 14:59, Bertram Felgenhauer wrote:
>>
>> I've misunderstood the problem. You intend to invoke old-style
>> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
>> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> 
> This may be premature, but I foresee that now that `isabelle ghc`
> and `isabelle ghci` exist, we will have scripts that use them.

There is indeed some confusion here.

My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained
by the odd recursive setup: in the stack situation, $ISABELLE_GHC points
to lib/Tools/ghc, and some mistake in the configuration could lead to
infinite recursion of sub-processes (potential bombing of the OS).

It is probably better to leave the meaning of ISABELLE_GHC (and
ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle
ghc" tool entry points: these auxiliary scripts should go into
$ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular
Isabelle tools.

I have now also learned that "ghci" is just "ghc --interactive", so
there is no point to treat it too prominently.


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

Re: [isabelle-dev] NEWS: support for GHC

[Bertram Felgenhauer]

Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> > Makarius wrote:
> >> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> >> Isabelle settings mechanism to override ISABELLE_GHC with the
> >> stack-based tools.
> > 
> > After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
> > a missing GHC setup, since there's no fallback on a custom
> > $ISABELLE_GHC. I've added such a fallback in the attached patch,
> > does that look reasonable?
> 
> I've misunderstood the problem. You intend to invoke old-style
> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.

This may be premature, but I foresee that now that `isabelle ghc`
and `isabelle ghci` exist, we will have scripts that use them.

> So just the usual question: What are remaining uses of this? Why not
> uninstall the "system ghc" and only use stack?

I don't think that the desire of using an existing ghc installation is
unusual. I'm not sure how common maintaining a ghc installation without
stack is these days, but ghc + cabal-install are still quite sufficient
for Haskell development. I don't care much about disk space, but I do
resent stack's propensity for downloading huge tarballs without even
prompting; my bandwidth is often limited. So I try hard to avoid that
particular tool.

> My impression is that up-to-date Haskell projects are all using stack by
> default.

My desire is to be able to override the default, not to change it.

Cheers,

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

Re: [isabelle-dev] NEWS: support for GHC

[Makarius]

On 08/11/2018 12:16, Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
>> Makarius wrote:
>>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>>> Isabelle settings mechanism to override ISABELLE_GHC with the
>>> stack-based tools.
>>
>> After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
>> a missing GHC setup, since there's no fallback on a custom
>> $ISABELLE_GHC. I've added such a fallback in the attached patch,
>> does that look reasonable?
> 
> I've misunderstood the problem. You intend to invoke old-style
> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> 
> So just the usual question: What are remaining uses of this? Why not
> uninstall the "system ghc" and only use stack? It should be possible to
> direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting
> out remaining problems on that side.
> 
> My impression is that up-to-date Haskell projects are all using stack by
> default.

A remaining use of "unmanaged" ghc is actually ocaml: I would like to
keep these tools as uniform as possible, see also current a41f49148525.
Unfortunately, OPAM is not as advanced as stack yet, e.g. it does not
quite work on Windows so the Cygwin ocaml is still needed.

We could move the other way and discontinue the meaning of $ISABELLE_GHC
and $ISABELLE_OCAMLC as actual executables: the settings would merely
indicate the presence of these tools, e.g. for options [condition =
ISABELLE_GHC] in session ROOT entries.

It probably would require some changes of the Codegen setup, because
that wants to see a single environment variable instead of a
command-line fragment like "isabelle ghc" or "isabelle ocamlc".


Makarius

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

Re: [isabelle-dev] NEWS: support for GHC

[Makarius]

On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> Makarius wrote:
>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>> Isabelle settings mechanism to override ISABELLE_GHC with the
>> stack-based tools.
> 
> After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
> a missing GHC setup, since there's no fallback on a custom
> $ISABELLE_GHC. I've added such a fallback in the attached patch,
> does that look reasonable?

I've misunderstood the problem. You intend to invoke old-style
$ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.

So just the usual question: What are remaining uses of this? Why not
uninstall the "system ghc" and only use stack? It should be possible to
direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting
out remaining problems on that side.

My impression is that up-to-date Haskell projects are all using stack by
default.


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

Re: [isabelle-dev] NEWS: support for GHC

[Bertram Felgenhauer]

Makarius wrote:
> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> Isabelle settings mechanism to override ISABELLE_GHC with the
> stack-based tools.

After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
a missing GHC setup, since there's no fallback on a custom
$ISABELLE_GHC. I've added such a fallback in the attached patch,
does that look reasonable?

Cheers,

Bertram
diff -r 0a9688695a1b lib/Tools/ghc
--- a/lib/Tools/ghc Thu Nov 08 09:11:52 2018 +0100
+++ b/lib/Tools/ghc Thu Nov 08 11:25:55 2018 +0100
@@ -6,6 +6,8 @@
 
 if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then
   isabelle_stack ghc -- "$@"
+elif [ -n "$ISABELLE_GHC" ]; then
+  "$ISABELLE_GHC" "$@"
 else
   echo "Cannot execute ghc: missing Isabelle GHC setup" >&2
   exit 127
diff -r 0a9688695a1b lib/Tools/ghci
--- a/lib/Tools/ghciThu Nov 08 09:11:52 2018 +0100
+++ b/lib/Tools/ghciThu Nov 08 11:25:55 2018 +0100
@@ -6,6 +6,8 @@
 
 if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then
   isabelle_stack ghci "$@"
+elif [ -n "$ISABELLE_GHC" ]; then
+  "$ISABELLE_GHC" --interactive "$@"
 else
   echo "Cannot execute ghci: missing Isabelle GHC setup" >&2
   exit 127
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: Isabelle/PIDE modules for Haskell

[Makarius]

*** System ***

* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
source modules for Isabelle tools implemented in Haskell, notably for
Isabelle/PIDE.


This refers e.g. to current Isabelle/438e1a11445f.

There is more and more material emerging: as direct ports from
Isabelle/ML using the our canonical naming conventions and functional
programming style.


I writing these sources with VSCode and the extension "Haskell Language
Server" 0.0.24, see also https://github.com/haskell/haskell-ide-engine

After several days of tinkering it now works fairly well for me, even
with friendly hints via hlint. Unfortunately I failed to reproduce the
installation on my mobile machine. This reminds a bit of ancient times
with vi and emacs, before Isabelle/PIDE/jEdit.


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

Re: [isabelle-dev] NEWS: support for GHC

[Makarius]

On 07/11/2018 16:32, Bertram Felgenhauer wrote:
> Makarius wrote:
>> *** System ***
>>
>> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
>> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
>> Existing settings variable ISABELLE_GHC is maintained dynamically
>> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
>>
>>
>> This refers to Isabelle/1722cc56d22e.
> 
> Is there a way to use a system ghc with `isabelle ghc` and
> `isabelle ghci`? I want to avoid the 145MB download and extra
> installation of ghc if possible.

The directory $ISABELLE_STACK_ROOT should be actually somewhat  bigger:
up to 5 GB for all the library modules. On Windows there is another
directory to take care of, according to "stack path programs".

I do prefer using up disk space and get a well-defined installation in
return. (I am presently working with someone building a Haskell-based
tool that is connected to Isabelle: the very first problem we had to
overcome was "cabal dependency hell". With stack it worked out nicely on
the spot, even on Windows and Mac OS X.)

Nonetheless, it is still possible to use "isabelle ghc" without stack:
you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
Isabelle settings mechanism to override ISABELLE_GHC with the
stack-based tools.


> Note in particular that setting ISABELLE_GHC now has a peculiar
> effect on `isabelle ghc`. Without the environment variable, the
> command complains:
> 
>   Cannot execute ghc: missing Isabelle GHC setup
> 
> However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings,
> then the same command starts downloading ghc via stack...

This should be more robust in current Isabelle/8bfa615ddde4 (the
relevant change is c911716d29bb).

You need to run "isabelle ghc_setup" once again to ensure that the extra
file "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS" is present --
otherwise it will fall back on old-style ISABELLE_GHC defaults despite
the presence of $ISABELLE_STACK_ROOT.


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

Re: [isabelle-dev] NEWS: support for GHC

[Bertram Felgenhauer]

Makarius wrote:
> *** System ***
> 
> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
> 
> 
> This refers to Isabelle/1722cc56d22e.

Is there a way to use a system ghc with `isabelle ghc` and
`isabelle ghci`? I want to avoid the 145MB download and extra
installation of ghc if possible.

Note in particular that setting ISABELLE_GHC now has a peculiar
effect on `isabelle ghc`. Without the environment variable, the
command complains:

  Cannot execute ghc: missing Isabelle GHC setup

However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings,
then the same command starts downloading ghc via stack...

  > isabelle ghc
  Preparing to install GHC (tinfo6) to an isolated location.
  This will not interfere with any system-level installation.
  Preparing to download ghc-tinfo6-8.4.4 ...^C

Given the size of the download I find this unsatisfactory
(145 MB is still big for mobile plans.)

Cheers,

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

Re: [isabelle-dev] NEWS: support for GHC

[David Matthews]

On 22/10/2018 14:05, Lars Hupel wrote:

The binary provided by Homebrew does not exhibit that problem. I have no
other information beyond that.


I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.

Interestingly enough, I get Poly/ML warnings of the form:

14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
failed (error code=3)
14:11:19 *** error: can't allocate region
14:11:19 *** set a breakpoint in malloc_error_break to debug



This is an Apple bug.  It produces this message if it can't allocate 
memory in certain situations.  That's a perfectly normal case and other 
operating systems just silently, and correctly, return zero from malloc. 
 Poly/ML deals with that.  Just ignore it.


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

Re: [isabelle-dev] NEWS: support for GHC

[Makarius]

On 22/10/2018 15:05, Lars Hupel wrote:
> 
> I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.
> 
> Interestingly enough, I get Poly/ML warnings of the form:
> 
> 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
> failed (error code=3)
> 14:11:19 *** error: can't allocate region
> 14:11:19 *** set a breakpoint in malloc_error_break to debug
> 
> This happens during the build of "HOL-Decision_Procs", which succeeds
> regardless:
> 
> 14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu
> time, factor 1.91)

This is a normal feature of memory management on macOS.

After all these years, David Matthews might eventually want to look if
it is still required these days: for that he merely needs regular SSH
access to some test machine.


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

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> The binary provided by Homebrew does not exhibit that problem. I have no
> other information beyond that.

I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.

Interestingly enough, I get Poly/ML warnings of the form:

14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
failed (error code=3)
14:11:19 *** error: can't allocate region
14:11:19 *** set a breakpoint in malloc_error_break to debug

This happens during the build of "HOL-Decision_Procs", which succeeds
regardless:

14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu
time, factor 1.91)

The timestamp suggests that this happens close to the end of the
session; although no heap image has to be saved for that session.

I'll run some more experiments to figure out if this is spurious or not.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> Can you actually explain the problem and its solution?

The problem appears to be that the official Stack binaries do not work
consistently on El Capitan. The machine I've tried them on is fully
updated and has no special software setup.

The binary provided by Homebrew does not exhibit that problem. I have no
other information beyond that.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: support for GHC

[Makarius]

On 21/10/2018 17:34, Lars Hupel wrote:
>> On an El Capitan system, this produces the following error:
> 
> The problem can alternatively be solved by installing Homebrew's stack
> version and declaring
> 
> ISABELLE_STACK="/usr/local/bin/stack"
> 
> in ~/.isabelle/etc/settings.

Can you actually explain the problem and its solution?


Makarius



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

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> On an El Capitan system, this produces the following error:

The problem can alternatively be solved by installing Homebrew's stack
version and declaring

ISABELLE_STACK="/usr/local/bin/stack"

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

Re: [isabelle-dev] NEWS: support for GHC

[Florian Haftmann]

> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.

Just a side remark: I have tried »isabelle ghc_setup« and
»isabelle_ocaml_setup« and they work like a charm.

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: support for GHC

[Makarius]

On 21/10/2018 13:25, Lars Hupel wrote:
>> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
>> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
>> Existing settings variable ISABELLE_GHC is maintained dynamically
>> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
> 
> On an El Capitan system, this produces the following error:
> 
> $ uname -a
> Darwin macisa1.in.tum.de 15.6.0 Darwin Kernel Version 15.6.0: Mon Aug 29
> 20:21:34 PDT 2016; root:xnu-3248.60.11~1/RELEASE_X86_64 x86_64
> 
> $ ./bin/isabelle ghc_setup
> /Users/hupel/workspace/isabelle/lib/scripts/getfunctions: line 1: 31569
> Illegal instruction: 4  env STACK_ROOT="$(platform_path
> "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"

Maybe there is something wrong with the hardware or the system installation.

It works fine on all Macs that are part of the official isabelle-dev
test infrastructure. See also Admin/PLATFORMS (Isabelle/c360f3b603f8):

  x86_64-darwin Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1)
macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
macOS 10.13 High Sierra (!?)
macOS 10.14 Mojave (!?)

This also shows that 10.13 and 10.14 are presently not covered: there
has been a general decline in Mac support in recent years. Isabelle on
macOS presently hinges on a somewhat pathetic Mac Mini that I have at home.

It would be great to recover some old vigor concerning isabelle-dev
platform coverage: via regular OS installations with regular SSH access.
Maybe even with nightly build_history measurements via isabelle_cronjob
(not Jenkins).


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

Re: [isabelle-dev] NEWS: support for GHC

[Lars Hupel]

> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.

On an El Capitan system, this produces the following error:

$ uname -a
Darwin macisa1.in.tum.de 15.6.0 Darwin Kernel Version 15.6.0: Mon Aug 29
20:21:34 PDT 2016; root:xnu-3248.60.11~1/RELEASE_X86_64 x86_64

$ ./bin/isabelle ghc_setup
/Users/hupel/workspace/isabelle/lib/scripts/getfunctions: line 1: 31569
Illegal instruction: 4  env STACK_ROOT="$(platform_path
"$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"

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

[isabelle-dev] NEWS: support for GHC

[Makarius]

*** System ***

* Support for Glasgow Haskell Compiler via command-line tools "isabelle
ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
Existing settings variable ISABELLE_GHC is maintained dynamically
according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.


This refers to Isabelle/1722cc56d22e.

The Haskell "stack" looks much more solid than OPAM. It works on Windows
without further ado, using native x86_64-windows personality.


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

Re: [isabelle-dev] NEWS: support for OCaml / OPAM

[Lars Hupel]

>   * How to re-init the opam installation, e.g. after changing
> ISABELLE_OCAML_VERSION (maybe even in ISABELLE_HOME_USER/etc/settings)?
> (Presently I have just removed purged ISABELLE_OPAM_ROOT.)

I don't think purging the directory is necessary. It should work out of
the box. According to my experiments, opam will just install another
OCaml version side-by-side.

>   * Is the update of ~/.ocamlinit that is proposed by opam init required?

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

[isabelle-dev] NEWS: CakeML compiler

[Lars Hupel]

This refers to AFP/c245a746483a and Isabelle/337b8ce5ff8d.

The CakeML compiler is now available from within Isabelle/ML.

Steps to use:

1) echo 'init_components "$HOME/.isabelle/contrib" 
"$ISABELLE_HOME/Admin/components/cakeml"' >> ~/.isabelle/etc/settings

2) echo 'ISABELLE_CC=gcc' >> ~/.isabelle/etc/settings
   (or clang, if you like)
3) isabelle components -a
4) import "CakeML.CakeML_Compiler" [*]
5) the command "cakeml" with the flags "literal" and "prog" is available

Examples:

cakeml (literal) ‹print "hi1";› (* prints "hi1" *)
cakeml (literal) ‹print "hi2";› (* prints "hi2" *)

(* this defines a HOL term that corresponds to a CakeML AST *)
definition simple_print :: Ast.prog where
"simple_print =
  [Ast.Tdec (Ast.Dlet default_loc Ast.Pany (Ast.App Ast.Opapp [Ast.Var 
(Short ''print''), Ast.Lit (Ast.StrLit ''hi'')]))]"


cakeml (prog) ‹simple_print› (* prints "hi" *)

How it works:

The bootstrapped CakeML compiler is available as a component that 
provides binaries for Linux and macOS. The steps to compile a CakeML 
program are as follows:


1) use "cake" to produce an assembly file "foo.S" from some input 
"foo.ml"
2) use "ISABELLE_CC" to compile the "basis_ffi.c" file to "basis_ffi.o" 
(provided by the CakeML component)

3) use "ISABELLE_CC" to link "basis_ffi.o" and "foo.S"

"cakeml (literal)" will take a cartouche that contains a literal CakeML 
program and invokes those steps.


"cakeml (prog)" will take a term. That term is evaluated through the 
code generator -- expecting a CakeML AST --, and then converted into a 
string. It will then do the same as above. The conversion into a string 
is very rudimentary at the moment. It only supports a tiny fraction of 
the CakeML abstract syntax.


Let me know if you run into any problems.

[*] Note that that theory is _not_ built when building the AFP unless 
the CakeML component is enabled and "ISABELLE_CC" is set. In a way, it's 
similar to the various "export_code ... checking" theories.

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

Re: [isabelle-dev] NEWS: discontinued old-style inner comments

[Makarius]

On 24/09/18 08:19, Lars Hupel wrote:
>> There were a few remaining uses in AFP. Notable changes are
>> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
>> generated by LEM (!). I don't know how LEM is maintained: it needs to
>> produce different inner comments next time, and can actually use
>> \ CARTOUCHE notation uniformly for inner and outer comments --
>> also note that this needs to be LaTeX-conformant, e.g. by another nested
>> cartouche or \<^verbatim>CARTOUCHE.
> 
> The way this works is that I'll have to send them a patch. This should
> hopefully be simple enough.

OK, thanks.


Makarius

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

Re: [isabelle-dev] NEWS: discontinued old-style inner comments

[Lars Hupel]

> There were a few remaining uses in AFP. Notable changes are
> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
> generated by LEM (!). I don't know how LEM is maintained: it needs to
> produce different inner comments next time, and can actually use
> \ CARTOUCHE notation uniformly for inner and outer comments --
> also note that this needs to be LaTeX-conformant, e.g. by another nested
> cartouche or \<^verbatim>CARTOUCHE.

The way this works is that I'll have to send them a patch. This should
hopefully be simple enough.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: discontinued old-style inner comments

[Makarius]

*** General ***

* Old-style inner comments (* ... *) within the term language are no
longer supported (legacy feature in Isabelle2018).


This refers to Isabelle/6e9df530b441.

There were a few remaining uses in AFP. Notable changes are
AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
generated by LEM (!). I don't know how LEM is maintained: it needs to
produce different inner comments next time, and can actually use
\ CARTOUCHE notation uniformly for inner and outer comments --
also note that this needs to be LaTeX-conformant, e.g. by another nested
cartouche or \<^verbatim>CARTOUCHE.


Now that (* ... *) is no longer part of the term language, Tobias can
finish the infix syntax update project, to get rid of the slightly odd
extra spaces for infixes with *.

There is also a chance that this will speed up the inner parser and/or
grammar updates, which happen quite often (e.g. for local syntax).


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

[isabelle-dev] NEWS: discontinued old-style goal cases

[Makarius]

*** Isar ***

* Implicit cases goal1, goal2, goal3, etc. have been discontinued
(legacy feature since Isabelle2016).


This refers to 8c240fdeffcb. The NEWS for Isabelle2016 already explain
that the proof method "goal_cases" is the proper way to do it.


Makarius

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

[isabelle-dev] NEWS: more support for other ML applications

[Makarius]

*** ML ***

* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").

* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
for Isabelle/ML, or "SML" for official Standard ML. It is also possible
to move toplevel bindings between environments, using a notation with
">" as separator. For example:

  declare [[ML_environment = "Isabelle>SML"]]
  ML ‹val println = writeln›

  declare [[ML_environment = "SML"]]
  ML ‹println "test"›

  declare [[ML_environment = "Isabelle"]]
  ML ‹println›  ― ‹not present›

The Isabelle/ML function ML_Env.setup defines new ML environments. This
is useful to incorporate big SML projects in an isolated name space, and
potentially with variations on ML syntax (existing ML_Env.SML_operations
observes the official standard).


This refers to Isabelle/7414ce0256e1.

It is the current state of various ongoing discussions about
incorporating other ML applications into the Isabelle environment (e.g.
OpenTheory, Metis, MetiTarski HOL4, ProofPower). There are two
motivations for this:

  (1) Developing these tools in the Isabelle Prover IDE
  (instead of vi or Emacs)

  (2) Using these tools inside Isabelle

A bit more work is required to make this really work in practice, but
this is an important stepping stone towards routine use of "ML
virtualization" (Isabelle can load Isabelle/Pure into itself, so it
should be able to load less complex applications, too).


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

[isabelle-dev] NEWS: document_tags (update)

[Makarius]

*** Document preparation ***

* System option "document_tags" specifies alternative command tags. This
is occasionally useful to control the global visibility of commands via
session options (e.g. in ROOT).


This refers to Isabelle/88b0e63d58a5, which also provides the updated
documentation. The motivation is the HOL-Analysis manual, which could
use options like this:

  document_variants = "document:manual=-proof,-ML,-unimportant"

  document_tags =
"theorem%important,corollary%important,proposition%important,%unimportant"

This means that the above theorem statements are visible by default, and
if their proof is not tagged otherwise it retains its default tagging.

In contrast, an explicit "lemma %important" in the text makes its proof
also important, and something like "proof %unimportant" will be required
to hide it.


That is a rather minimal change to the previous version of
document_tags, and hopefully sufficient for the release.

Here are further spots for improvement (after the release):

  * improved handling of whitespace surrounding hidden material

  * improved handling (replacement?) of old (*<*)...(*>*) vs. tags

  * ways to specify command tags for a whole region of text (maybe just
in the Prover IDE, not in the source)


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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

I just tried

isabelle jedit -R HOL-UNITY

assuming that it would build an auxiliary image for HOL-Auth, which is 
imported. It built HOL-Auth rather than HOL-UNITY_requirements(HOL-Auth) so 
things are pretty subtle here. A little more explanation would be valuable.

Larry

> On 6 Jun 2018, at 16:36, Makarius  wrote:
> 
> It could just mean that these examples don't need an auxiliary image.
> 
> Take the first example from NEWS:
> 
>  isabelle jedit -R HOL-Number_Theory
> 
> It produces an image
> "HOL-Number_Theory_requirements(HOL-Computational_Algebra)", see also
> the title line of Isabelle/jEdit.
> 
> It also puts you into the ROOT entry for HOL-Number_Theory, so you can
> directly explore its theories in the Prover IDE.

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Makarius]

On 06/06/18 16:19, Lawrence Paulson wrote:
> 
> According to the NEWS entry, option -R builds an auxiliary logic image. I 
> tried this with a couple of examples and no images were built. According to 
> the manual, this option opens the ROOT entry. It does seem to do that, though 
> I'm not sure why this facility is needed.
> 

It could just mean that these examples don't need an auxiliary image.

Take the first example from NEWS:

  isabelle jedit -R HOL-Number_Theory

It produces an image
"HOL-Number_Theory_requirements(HOL-Computational_Algebra)", see also
the title line of Isabelle/jEdit.

It also puts you into the ROOT entry for HOL-Number_Theory, so you can
directly explore its theories in the Prover IDE.


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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

> On 6 Jun 2018, at 12:43, Makarius  wrote:
> 
> On 06/06/18 12:45, Lawrence Paulson wrote:
>> I saw them of course, but what do they do?
> 
> These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
> have simplified and clarified the situation, updated NEWS and
> documentation in the "jedit" manual.
> 
> Right now the main question is if this is sufficient for the release,
> and the documentation clear.

Having tinkered with these things, read the NEWS entry and read the relevant 
section of the manual, I am still completely in the dark.

According to the NEWS entry, option -R builds an auxiliary logic image. I tried 
this with a couple of examples and no images were built. According to the 
manual, this option opens the ROOT entry. It does seem to do that, though I'm 
not sure why this facility is needed.

Surely it wouldn't be difficult to add a few lines of text, describing the sort 
of situation in which this option is useful.

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Makarius]

On 06/06/18 12:45, Lawrence Paulson wrote:
> I saw them of course, but what do they do?

These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
have simplified and clarified the situation, updated NEWS and
documentation in the "jedit" manual.

Right now the main question is if this is sufficient for the release,
and the documentation clear.


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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Fabian Immler]

> Am 05.06.2018 um 23:01 schrieb Makarius :
> 
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further refinement.
> 
> In other words, the question behind this: Can be get rid of most
> auxiliary images in AFP (e.g. "Foo_Lib", "Pre_Foo")?
I started to use -S HOL-ODE-Numerics and got rid of HOL-ODE-Refinement (which 
was such an auxiliary image) in AFP/cf739ca.
-S is very helpful because it reduces the start-up time for Isabelle/jEdit 
(with the AFP in ROOTS) from 100s to 30s (compared to -R).

I can also imagine that auxiliary images get outdated easily (importing too 
much or too little), and so it is good that -R/-S takes care of this potential 
maintenance efforts.

Fabian

smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

I saw them of course, but what do they do?
Larry

> On 5 Jun 2018, at 22:19, Makarius  wrote:
> 
> On 05/06/18 23:06, Lawrence Paulson wrote:
>> I’d find an example helpful, as your brief description is pretty cryptic.
>> Larry
>> 
>>> On 5 Jun 2018, at 22:01, Makarius  wrote:
>>> 
>>> These options are very relevant for the coming release. I am interested
>>> to get feedback from early adopters, if this is already sufficient or
>>> requires further refinement.
> 
> The NEWS contains these examples:
> 
>  Examples:
>isabelle jedit -R HOL-Number_Theory
>isabelle jedit -R HOL-Number_Theory -A HOL
>isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
>isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
> 
> Here are more examples:
> 
>isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Analysis
>isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Probability
>isabelle jedit -d '$AFP' -S Deep_Learning
> 
> Alexander Bentkamp needs to be credited for writing a clear
> specification of the intermediate image Deep_Learning_Lib: {* Theories
> that are not part of HOL-Probability but are used by this entry *}.
> 
> From there it was reasonably easy to implement the above options, but
> users need to start using them, and stop publishing old development
> artefacts in AFP.
> 
> 
>   Makarius

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Makarius]

On 05/06/18 23:06, Lawrence Paulson wrote:
> I’d find an example helpful, as your brief description is pretty cryptic.
> Larry
> 
>> On 5 Jun 2018, at 22:01, Makarius  wrote:
>>
>> These options are very relevant for the coming release. I am interested
>> to get feedback from early adopters, if this is already sufficient or
>> requires further refinement.

The NEWS contains these examples:

  Examples:
isabelle jedit -R HOL-Number_Theory
isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis

Here are more examples:

isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Analysis
isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Probability
isabelle jedit -d '$AFP' -S Deep_Learning

Alexander Bentkamp needs to be credited for writing a clear
specification of the intermediate image Deep_Learning_Lib: {* Theories
that are not part of HOL-Probability but are used by this entry *}.

From there it was reasonably easy to implement the above options, but
users need to start using them, and stop publishing old development
artefacts in AFP.


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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

I’d find an example helpful, as your brief description is pretty cryptic.
Larry

> On 5 Jun 2018, at 22:01, Makarius  wrote:
> 
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further refinement.

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Makarius]

On 04/06/18 14:27, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
> 
> * The command-line tool "isabelle jedit" provides more flexible options
> for session management:
>   - option -R builds an auxiliary logic image with all required theories
> from other sessions, relative to an ancestor session given by option
> -A (default: parent)
>   - option -S is like -R, with a focus on the selected session and its
> descendants (this reduces startup time for big projects like AFP)
> 
>   Examples:
> isabelle jedit -R HOL-Number_Theory
> isabelle jedit -R HOL-Number_Theory -A HOL
> isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
> isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
> 
> 
> This refers to Isabelle/bcdc47c9d4af, it is a clarification and
> simplification from earlier options. That changeset also contains the
> updated documentation.

These options are very relevant for the coming release. I am interested
to get feedback from early adopters, if this is already sufficient or
requires further refinement.

In other words, the question behind this: Can be get rid of most
auxiliary images in AFP (e.g. "Foo_Lib", "Pre_Foo")?

Typically they just slow down the build process -- due to reduced
parallelism and extra file-system operations to compact/store/load the
intermediate image.


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

Re: [isabelle-dev] NEWS: sightly more parallel checking

[Makarius]

On 05/06/18 14:54, Fabian Immler wrote:
> 
>> What kind of theory is this? Many commands? Long-running /
>> non-terminating commands?
> In this particular case, it was a relatively short theory (300 lines) with no 
> long-running or non-terminating commands. I inserted and removed some 
> diagnostic commands (code_thms, export_code foo in SML), but those were not 
> present anymore when I observed this 4-second-consolidation-loop.

The consolidation operates on the whole theory graph, even if relatively
little has actually happened. For a large session this might be expensive.

I have now changed this in Isabelle/2fd3a6d6ba2e, and tested it with
HOL-Library, HOL-Analysis, HOL-Probability, even with updates of the
State panel in between.

So far it looks good to me. Please keep me updated if there are
remaining problems.


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

Re: [isabelle-dev] NEWS: sightly more parallel checking

[Fabian Immler]

> Am 05.06.2018 um 14:47 schrieb Makarius :
> 
> On 05/06/18 14:45, Fabian Immler wrote:
>> 
>> 
 The only way to stop this apparently is to invalidate something in the
 beginning of the (currently open) theory.
>>> 
>>> It should be possible to achieve this effect by removing the concluding
>>> 'end' command.
>> Just now I was in the middle of a theory (without any 'end' command), where 
>> every (are they supposed to happen periodically?) "consolidation" took about 
>> 4 seconds.
>> 
>> It seems like something is accumulating somewhere when editing the document, 
>> because after invalidating the beginning of the theory and going back to the 
>> same place as before, the "consolidation" was not noticeable any more.
> 
> What kind of theory is this? Many commands? Long-running /
> non-terminating commands?
In this particular case, it was a relatively short theory (300 lines) with no 
long-running or non-terminating commands. I inserted and removed some 
diagnostic commands (code_thms, export_code foo in SML), but those were not 
present anymore when I observed this 4-second-consolidation-loop.

Fabian

smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: sightly more parallel checking

[Makarius]

On 05/06/18 14:45, Fabian Immler wrote:
> 
> 
>>> The only way to stop this apparently is to invalidate something in the
>>> beginning of the (currently open) theory.
>>
>> It should be possible to achieve this effect by removing the concluding
>> 'end' command.
> Just now I was in the middle of a theory (without any 'end' command), where 
> every (are they supposed to happen periodically?) "consolidation" took about 
> 4 seconds.
> 
> It seems like something is accumulating somewhere when editing the document, 
> because after invalidating the beginning of the theory and going back to the 
> same place as before, the "consolidation" was not noticeable any more.

What kind of theory is this? Many commands? Long-running /
non-terminating commands?


Makarius

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

Re: [isabelle-dev] NEWS: sightly more parallel checking

[Fabian Immler]

> Am 05.06.2018 um 13:39 schrieb Makarius :
> 
> On 04/06/18 20:17, Fabian Immler wrote:
>> 
>> This "something in the background" appears to happen on a regular basis:
>> every 2-3 seconds, the poly process consumes 200%CPU for about a second.
>> poly should be idle (or used to be in such a situation) because (as far
>> as I can tell) nothing else (e.g., sledgehammer, find theorems) seems to
>> be active.
> 
> This is probably due to the implicit "consolidation" of finished
> theories, which I have made a bit more official as PIDE document edit
> (see Isabelle/09ac56914b29). That is important, because of the final
> "presentation", e.g. for generated LaTeX.
> 
> In Isabelle/38272f9481c2, I have also changed the delay from 1s to 2.5s
> -- you can make this 10s or more until I figure out a way to reduce the
> impact of it.
Thanks, this really seems to be the "consolidation": I can see the effect of 
chainging editor_consolidate_delay.

>> The only way to stop this apparently is to invalidate something in the
>> beginning of the (currently open) theory.
> 
> It should be possible to achieve this effect by removing the concluding
> 'end' command.
Just now I was in the middle of a theory (without any 'end' command), where 
every (are they supposed to happen periodically?) "consolidation" took about 4 
seconds.

It seems like something is accumulating somewhere when editing the document, 
because after invalidating the beginning of the theory and going back to the 
same place as before, the "consolidation" was not noticeable any more.

Fabian




smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: sightly more parallel checking

[Makarius]

On 04/06/18 20:17, Fabian Immler wrote:
> 
> This "something in the background" appears to happen on a regular basis:
> every 2-3 seconds, the poly process consumes 200%CPU for about a second.
> poly should be idle (or used to be in such a situation) because (as far
> as I can tell) nothing else (e.g., sledgehammer, find theorems) seems to
> be active.

This is probably due to the implicit "consolidation" of finished
theories, which I have made a bit more official as PIDE document edit
(see Isabelle/09ac56914b29). That is important, because of the final
"presentation", e.g. for generated LaTeX.

In Isabelle/38272f9481c2, I have also changed the delay from 1s to 2.5s
-- you can make this 10s or more until I figure out a way to reduce the
impact of it.


> The only way to stop this apparently is to invalidate something in the
> beginning of the (currently open) theory.

It should be possible to achieve this effect by removing the concluding
'end' command.


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

[isabelle-dev] NEWS: isabelle jedit options

[Makarius]

*** Isabelle/jEdit Prover IDE ***

* The command-line tool "isabelle jedit" provides more flexible options
for session management:
  - option -R builds an auxiliary logic image with all required theories
from other sessions, relative to an ancestor session given by option
-A (default: parent)
  - option -S is like -R, with a focus on the selected session and its
descendants (this reduces startup time for big projects like AFP)

  Examples:
isabelle jedit -R HOL-Number_Theory
isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis


This refers to Isabelle/bcdc47c9d4af, it is a clarification and
simplification from earlier options. That changeset also contains the
updated documentation.


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

[isabelle-dev] NEWS: sightly more parallel checking

[Makarius]

*** Isabelle/jEdit Prover IDE ***

* Slightly more parallel checking, notably for high priority print
functions (e.g. State output).


This refers to Isabelle/b00b40dc41af -- with various fine points in the
organization of PIDE execution forks, not just the preceeding cd387c55e085.

As we are heading towards the release, it is important to keep an eye on
the system, that everything works smoothly. I will try not to touch more
such delicate points of PIDE document processing.


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

[isabelle-dev] NEWS: isabelle dump

[Makarius]

*** System ***

* The command-line tool "dump" dumps information from the cumulative
PIDE session database: many sessions may be loaded into a given logic
image, results from all loaded theories are written to the output
directory.


This refers to Isabelle/2ac3a5c07dfa. It is a spin-off from various
subtle changes of PIDE session management, the Thy_Resources session
from the "isabelle server", and the blob export facility. It also
depends on the session-qualified theory reform from the last release.

The section about "isabelle dump" in the "system" manual contains
further explanations with examples. Just for the fun of it, here is
another one (lxcisa0, threads=6):

  ISABELLE_TOOL_JAVA_OPTIONS=-Djava.awt.headless=true -Xms2g -Xmx32g -Xss16m

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/isabelle/contrib/polyml-5.7.1-5/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

  isabelle dump -v -l Pure -B HOL-Analysis -d '$AFP'
  6:03:34 elapsed time, 20:50:34 cpu time, factor 3.44
  6.2G dump

These are all sessions connected to HOL-Analysis, starting from Pure;
overall 1121 theories. Thus we can now fill our file-systems with funny
YXML data. It also shows how far we are in the project "Prover IDE for
all of AFP as one big document", here as a headless version.

Actual applications of this should come eventually: over the years
people have often asked me how to externalize PIDE markup and turn it
into some use elsewhere, lets say for formal data mining. Another
application could be OpenTheory export, but that also works with plain
"isabelle build" + "isabelle export", instead of the more ambitious
"isabelle dump -A theory".


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

[isabelle-dev] NEWS: command 'ML_export'

[Makarius]

*** ML ***

* Command 'ML_export' exports ML toplevel bindings to the global
bootstrap environment of the ML process. This allows ML evaluation
without a formal theory context, e.g. in command-line tools like
"isabelle process".


This refers to Isabelle/cbee43ff4ceb.

Here are also the examples from the "system" manual in
Isabelle/b5d0318757f0:

  isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'
  isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'

In other words, it is now quite easy to produce clean command-line
tools, based on ML functions inside a regular Isabelle session.


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

Re: [isabelle-dev] NEWS: Isabelle server

[Christian Sternagel]

Just for the record: Makarius' reply resolved the issue for me (see also
below).

On 05/09/2018 11:57 PM, Makarius wrote:
> On 26/03/18 13:48, Christian Sternagel wrote:
>>
>> Thanks, I forgot about that option.
>>
>> With "isabelle latex" in the specified directory the error boils down to:
>>
>> ./root.tex:31: Package pdftex.def Error: File
>> `isabelle-eps-converted-to.pdf' n
>> ot found.
>>
>> See the pdftex.def package documentation for explanation.
>> Type  H   for immediate help.
>>  ...
>>
>> Should isabelle-eps-converted-to.pdf exist on my system?
> 
> I guess that the "epstopdf" tool is missing: there should be some Fedora
> package for it.

That is correct. Thanks for pointing it out, it was not clear to me from
the error message.

> 
> Anyway, in Isabelle/2a5ae592eafb the latex errors are again spilled into
> user output -- this is required for hard errors of missing executables
> and style files.
> 
> With that I have managed to do "isabelle build -o document=pdf -g doc"
> or "isabelle build_doc -a" sucessfully on Fedora 28: after cumbersome
> saturation of the texlive installation, where almost every style file
> has its own package.

This kind of saturation is indeed cumbersome, but at least its possible
as long as you know which packages are missing ;)

cheers

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

Re: [isabelle-dev] NEWS: Isabelle server

[Makarius]

On 26/03/18 13:48, Christian Sternagel wrote:
> 
> Thanks, I forgot about that option.
> 
> With "isabelle latex" in the specified directory the error boils down to:
> 
> ./root.tex:31: Package pdftex.def Error: File
> `isabelle-eps-converted-to.pdf' n
> ot found.
> 
> See the pdftex.def package documentation for explanation.
> Type  H   for immediate help.
>  ...
> 
> Should isabelle-eps-converted-to.pdf exist on my system?

I guess that the "epstopdf" tool is missing: there should be some Fedora
package for it.

Anyway, in Isabelle/2a5ae592eafb the latex errors are again spilled into
user output -- this is required for hard errors of missing executables
and style files.

With that I have managed to do "isabelle build -o document=pdf -g doc"
or "isabelle build_doc -a" sucessfully on Fedora 28: after cumbersome
saturation of the texlive installation, where almost every style file
has its own package.


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

[isabelle-dev] NEWS: jedit-5.5.0

[Makarius]

*** Isabelle/jEdit Prover IDE ***

* Update to jedit-5.5.0, the latest release.


This refers to Isabelle/752a4e6d760c. Relatively little has happened,
but there are some preparations for Java 9. We are still on Java 8, even
though Java 10 has been released recently. I will soon make some
experiments to see if we can bump the Java version.

A notably change in jedit-5.5.0 is the patch by Rafal Kolanski:
https://www.sourceforge.net/p/jedit/patches/569/ -- it has only required
2.5 years to get into the code base.


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

Re: [isabelle-dev] NEWS: Isabelle server

[Christian Sternagel]

Dear Makarius,

Thanks, I forgot about that option.

With "isabelle latex" in the specified directory the error boils down to:

./root.tex:31: Package pdftex.def Error: File
`isabelle-eps-converted-to.pdf' n
ot found.

See the pdftex.def package documentation for explanation.
Type  H   for immediate help.
 ...

Should isabelle-eps-converted-to.pdf exist on my system?

cheers

chris

On 03/26/2018 01:26 PM, Makarius wrote:
> On 26/03/18 09:33, Christian Sternagel wrote:
>>
>> I don't see a significant difference in output between my original
>>
>>   isabelle build_doc system
> 
>> *** Failed to build document in
>> "/tmp/isabelle-griff/document_output1585848392449927242/system"
>>
>> and the suggested
>>
>>   isabelle build -c -b System -o document=pdf -o document_output=output
>>
>> *** Failed to build document in
>> "/home/griff/repos/tools/isabelle/src/Doc/System/output/system"
>>
>> I am still unclear on why "isabelle document" fails in both cases.
> 
> The difference is the output directory. In the latter situation, you can
> go there and inspect root.log or run pdflatex root manually.
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Isabelle server

[Makarius]

On 26/03/18 09:33, Christian Sternagel wrote:
> 
> I don't see a significant difference in output between my original
> 
>   isabelle build_doc system

> *** Failed to build document in
> "/tmp/isabelle-griff/document_output1585848392449927242/system"
> 
> and the suggested
> 
>   isabelle build -c -b System -o document=pdf -o document_output=output
>
> *** Failed to build document in
> "/home/griff/repos/tools/isabelle/src/Doc/System/output/system"
> 
> I am still unclear on why "isabelle document" fails in both cases.

The difference is the output directory. In the latter situation, you can
go there and inspect root.log or run pdflatex root manually.


Makarius

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

Re: [isabelle-dev] NEWS: Isabelle server

[Christian Sternagel]

Dear Makarius,

I don't see a significant difference in output between my original

  isabelle build_doc system

where I get

...
isabelle document -d
/tmp/isabelle-griff/document_output1585848392449927242/system -o pdf -n
system
*** Failed to build document in
"/tmp/isabelle-griff/document_output1585848392449927242/system"

and the suggested

  isabelle build -c -b System -o document=pdf -o document_output=output

where I get

...
isabelle document -d output/system -o pdf -n system
*** Failed to build document in
"/home/griff/repos/tools/isabelle/src/Doc/System/output/system"

I am still unclear on why "isabelle document" fails in both cases.

cheers

chris

PS: Anyway, I can get the manual from the URL you provided. Thanks!

On 03/23/2018 11:51 AM, Makarius wrote:
> On 23/03/18 10:29, Christian Sternagel wrote:
>>
>> Is there a way to get a more detailed report on why the last step,
>> "isabelle document ...",  failed?
>>
>> Btw: I also get (sometimes more specific) errors for building other
>> documentation.
>>
>> Okay, turns out that I was missing the LaTeX packages
>>
>>   nomencl, regexpatch, subfigure, supertabular
>>
>> on my system (Fedora 27). After installing those I still get some errors
>> (all with similar error message):
> 
> You can build all docs with detailed results like this:
> 
>   isabelle build -c -g doc -o document=pdf -o document_output=output
> 
> 
> For the purpose of the updated system manual, you can now download the
> nightly snapshot: https://isabelle.sketis.net/devel/release_snapshot
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Isabelle server

[Makarius]

On 23/03/18 10:29, Christian Sternagel wrote:
> 
> Is there a way to get a more detailed report on why the last step,
> "isabelle document ...",  failed?
> 
> Btw: I also get (sometimes more specific) errors for building other
> documentation.
> 
> Okay, turns out that I was missing the LaTeX packages
> 
>   nomencl, regexpatch, subfigure, supertabular
> 
> on my system (Fedora 27). After installing those I still get some errors
> (all with similar error message):

You can build all docs with detailed results like this:

  isabelle build -c -g doc -o document=pdf -o document_output=output


For the purpose of the updated system manual, you can now download the
nightly snapshot: https://isabelle.sketis.net/devel/release_snapshot


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

Re: [isabelle-dev] NEWS: Isabelle server

[Christian Sternagel]

Dear Makarius,

I am on 67927:0b70405b3969 and

  ./bin/isabelle build_doc system

doesn't work for me. I get the error:

  Build started for documentation "system"
  Cleaning System ...
  Running System ...
  System FAILED
  ...
  isabelle document -d
/tmp/isabelle-griff/document_output14698640433302927/system -o pdf -n system
  *** Failed to build document in
"/tmp/isabelle-griff/document_output14698640433302927/system"
  Unfinished session(s): System

Is there a way to get a more detailed report on why the last step,
"isabelle document ...",  failed?

Btw: I also get (sometimes more specific) errors for building other
documentation.

Okay, turns out that I was missing the LaTeX packages

  nomencl, regexpatch, subfigure, supertabular

on my system (Fedora 27). After installing those I still get some errors
(all with similar error message):

  Running Tutorial ...
  Tutorial FAILED
  ...
  isabelle document -d
/tmp/isabelle-griff/document_output1759007754075439311/tutorial -o pdf
-n tutorial
  *** Failed to build document in
"/tmp/isabelle-griff/document_output1759007754075439311/tutorial"
  Isar_Ref FAILED
  ...
  Codegen FAILED
  ...
  Prog_Prove FAILED
  ...
  Implementation FAILED
  ...
  Classes FAILED
  ...
  Eisbach FAILED
  ...
  Intro FAILED
  ...
  JEdit FAILED
  ...
  Logics FAILED
  ...
  Logics_ZF FAILED
  ...
  Nitpick FAILED
  ...
  Sledgehammer FAILED
  ...
  System FAILED
  ...
  Typeclass_Hierarchy FAILED

cheers

chris

On 03/22/2018 05:30 PM, Makarius wrote:
> On 19/03/18 19:35, Makarius wrote:
>> *** System ***
>>
>> * The command-line tools "isabelle server" and "isabelle client" provide
>> access to the Isabelle Server: it supports responsive session management
>> and concurrent use of theories, based on Isabelle/PIDE infrastructure.
>> See also the "system" manual.
>>
>>
>> This refers to Isabelle/465f43a9f780. The chapter in the "system" manual
>> provides general explanations, but lacks the description of specific
>> server commands: these may be derived from
>> src/Pure/Tools/server_commands.scala right now.
> 
> I have made further refinements in Isabelle/0b70405b3969. The chapter in
> the "system" manual now has almost 20 pages of explanations, including
> various examples, see
> http://isabelle.in.tum.de/repos/isabelle/file/0b70405b3969/src/Doc/System/Server.thy
> or better its LaTeX rendering (e.g. via "isabelle build_doc system &&
> isabelle doc system").
> 
> The server should already be usable, but the following fine points are
> still missing:
> 
>   * command "purge_theories" to get rid of results from "use_theories"
> 
>   * command "session_status" to provide continuous node_status
> information, similar to the Theories dockable in Isabelle/jEdit
> 
> 
>> It is only the start of a serious server, many more ideas are still in
>> the pipeline, e.g. forwarding over an SSH tunnel that may
>> disconnect/reconnect spontaneously.
> 
> The SSH tunnel will require more work. It practically needs a way to
> send theory files from the client OS context to the server OS context.
> (All tools for that are there in Isabelle/Scala, but need to be fit
> together in the proper way.)
> 
> 
>   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: Isabelle server

[Makarius]

On 19/03/18 19:35, Makarius wrote:
> *** System ***
> 
> * The command-line tools "isabelle server" and "isabelle client" provide
> access to the Isabelle Server: it supports responsive session management
> and concurrent use of theories, based on Isabelle/PIDE infrastructure.
> See also the "system" manual.
> 
> 
> This refers to Isabelle/465f43a9f780. The chapter in the "system" manual
> provides general explanations, but lacks the description of specific
> server commands: these may be derived from
> src/Pure/Tools/server_commands.scala right now.

I have made further refinements in Isabelle/0b70405b3969. The chapter in
the "system" manual now has almost 20 pages of explanations, including
various examples, see
http://isabelle.in.tum.de/repos/isabelle/file/0b70405b3969/src/Doc/System/Server.thy
or better its LaTeX rendering (e.g. via "isabelle build_doc system &&
isabelle doc system").

The server should already be usable, but the following fine points are
still missing:

  * command "purge_theories" to get rid of results from "use_theories"

  * command "session_status" to provide continuous node_status
information, similar to the Theories dockable in Isabelle/jEdit


> It is only the start of a serious server, many more ideas are still in
> the pipeline, e.g. forwarding over an SSH tunnel that may
> disconnect/reconnect spontaneously.

The SSH tunnel will require more work. It practically needs a way to
send theory files from the client OS context to the server OS context.
(All tools for that are there in Isabelle/Scala, but need to be fit
together in the proper way.)


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

[isabelle-dev] NEWS: Isabelle server

[Makarius]

*** System ***

* The command-line tools "isabelle server" and "isabelle client" provide
access to the Isabelle Server: it supports responsive session management
and concurrent use of theories, based on Isabelle/PIDE infrastructure.
See also the "system" manual.


This refers to Isabelle/465f43a9f780. The chapter in the "system" manual
provides general explanations, but lacks the description of specific
server commands: these may be derived from
src/Pure/Tools/server_commands.scala right now.

It is only the start of a serious server, many more ideas are still in
the pipeline, e.g. forwarding over an SSH tunnel that may
disconnect/reconnect spontaneously.

Various people who want to build tools on top of Isabelle have asked
about a proper server recently, so this is the opportunity to get
started using it, while it slowly stabilizes towards the Isabelle2018
release (approx. August 2018).


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