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] Analysis not building

[Bertram Felgenhauer]

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.

Neither can I; using polyml-b68438d33c69 I can build HOL-Analysis
with Isabelle-24bbc4e30e5b and manual init-component for Poly/ML and
both HOL-Analysis and IsaFoR with Isabelle-2018 and the same manual
init-component.

Maybe this is somehow specific to OS/X, which I believe Larry uses?

That said, polyml-1b2dcf8f5202 seems to work just as well, for me. 

In other news, the problem with the sharing pass appears to be resolved
and the IsaFoR images with x86_64_32 are now all about 60% the size of
the x86_64 ones. Nice!

Cheers,

Bertram

Numbers:

ML_PLATFORM="x86_64_32-linux"
ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6"
ISABELLE_BUILD_OPTIONS="threads=10 parallel_proofs=2"

polyml-test-1b2dcf8f5202
polyml-test-b68438d33c69


Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)
Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)

Finished HOL (0:02:23 elapsed time, 0:08:49 cpu time, factor 3.68)
Finished HOL (0:02:26 elapsed time, 0:08:58 cpu time, factor 3.69)

Finished HOL-Lib (0:05:12 elapsed time, 0:32:06 cpu time, factor 6.17)
Finished HOL-Lib (0:04:58 elapsed time, 0:31:08 cpu time, factor 6.25)

Finished HOL-AFP (0:05:40 elapsed time, 0:32:52 cpu time, factor 5.79)
Finished HOL-AFP (0:05:38 elapsed time, 0:32:51 cpu time, factor 5.82)

Finished IsaFoR_1 (0:05:10 elapsed time, 0:27:31 cpu time, factor 5.32)
Finished IsaFoR_1 (0:05:11 elapsed time, 0:27:39 cpu time, factor 5.33)

Finished IsaFoR_2 (0:05:26 elapsed time, 0:25:37 cpu time, factor 4.71)
Finished IsaFoR_2 (0:05:27 elapsed time, 0:25:37 cpu time, factor 4.69)

Finished IsaFoR_3 (0:06:38 elapsed time, 0:39:22 cpu time, factor 5.92)
Finished IsaFoR_3 (0:06:36 elapsed time, 0:39:24 cpu time, factor 5.96)

Finished IsaFoR_4 (0:08:26 elapsed time, 0:26:28 cpu time, factor 3.14)
Finished IsaFoR_4 (0:08:37 elapsed time, 0:26:55 cpu time, factor 3.12)

Finished Code (0:08:03 elapsed time, 0:08:11 cpu time, factor 1.02)
Finished Code (0:08:02 elapsed time, 0:08:11 cpu time, factor 1.02)

 19271289 Pure (0.69 x 28081037 (x86_64 heap image size))
 19269857 Pure (0.69)

250024211 HOL (0.61 x 410972244)
250129275 HOL (0.61)

307851090 HOL-Lib (0.59 x 525949867)
307921910 HOL-Lib (0.59)

537798522 HOL-AFP (0.59 x 913422879)
537694918 HOL-AFP (0.59)

428162386 IsaFoR_1 (0.59 x 724672759)
427425094 IsaFoR_1 (0.59)

367783763 IsaFoR_2 (0.59 x 623083120)
367626511 IsaFoR_2 (0.59)

419599023 IsaFoR_3 (0.59 x 712211696)
419246195 IsaFoR_3 (0.59)

284804855 IsaFoR_4 (0.59 x 480209352)
284701607 IsaFoR_4 (0.59)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev