Re: [isabelle-dev] Analysis not building
On 02/02/2019 15:37, Lawrence Paulson wrote: > This worked — thanks! > >> On 2 Feb 2019, at 13:56, Makarius wrote: >> >> Can you try the following in your $ISABELLE_HOME_USER/etc/settings? >> >> init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" OK. With Isabelle/76f2d492627e this is the default, and it is better to remove the init_component from local etc/settings again, to participate in further updates of the default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
This worked — thanks! Larry > On 2 Feb 2019, at 13:56, Makarius wrote: > > Can you try the following in your $ISABELLE_HOME_USER/etc/settings? > > init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" > > Apparently, the last two updates on polyml-test were not as monotonic as > I was hoping, despite clear improvements by David Matthews. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
On 02/02/2019 14:56, Makarius wrote: > On 02/02/2019 14:39, Lawrence Paulson wrote: >> It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle >> jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. >> >> The reason I fetched in the first place was that I was getting crashes in my >> interactive sessions. > > Can you try the following in your $ISABELLE_HOME_USER/etc/settings? > > init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" > > Apparently, the last two updates on polyml-test were not as monotonic as > I was hoping, despite clear improvements by David Matthews. > > After a standard test, I will probably make the above version the > default again. I've done that now in Isabelle/dde776d1defa, after successful "isabelle build -a". Thus we are at least back to the status-quo from some days ago, where nobody noticed everyday crashes. 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
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] Analysis not building
On 02/02/2019 14:39, Lawrence Paulson wrote: > It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle > jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. > > The reason I fetched in the first place was that I was getting crashes in my > interactive sessions. Can you try the following in your $ISABELLE_HOME_USER/etc/settings? init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" Apparently, the last two updates on polyml-test were not as monotonic as I was hoping, despite clear improvements by David Matthews. After a standard test, I will probably make the above version the default again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. The reason I fetched in the first place was that I was getting crashes in my interactive sessions. Larry > On 2 Feb 2019, at 13:26, Florian Haftmann > wrote: > >> HOL-Analysis can’t be built (reproducibly) with the latest version >> (76f2d492627e). It simply dies, no error message. > > I cannot reproduce this. > > ML_PLATFORM="x86_64_32-linux" > ML_SYSTEM="polyml-5.7.1" > ML_OPTIONS="--maxheap 9G" > > Have you tried a fresh build or delete the corresponding log / saved > state manually? > > Cheers, > Florian > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
> HOL-Analysis can’t be built (reproducibly) with the latest version > (76f2d492627e). It simply dies, no error message. I cannot reproduce this. ML_PLATFORM="x86_64_32-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="--maxheap 9G" Have you tried a fresh build or delete the corresponding log / saved state manually? 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
>> 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
[isabelle-dev] Analysis not building
HOL-Analysis can’t be built (reproducibly) with the latest version (76f2d492627e). It simply dies, no error message. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
