[isabelle-dev] polyml-test-b68438d33c69
With Isabelle/76f2d492627e we are on polyml-test-b68438d33c69: it is already fairly stable, but there are still some sporadic crashes, notably on slow machines (e.g. for "isabelle build HOL" on lxbroy10 or my macMini at home). On high-end machines, I can build all of Isabelle + AFP without problems. We do continue monotonically towards a stable Poly/ML version: David Matthews has already sorted out various subtle issues on https://github.com/polyml/polyml/commits/master -- leading up to current b68438d33c69. 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 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
> 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
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
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
> 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
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
> 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
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
> 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
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
