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

2019-02-04 Thread 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

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

2019-02-04 Thread 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

[isabelle-dev] Uniform Isabelle repository clones via https://isabelle.sketis.net/repos

2019-02-04 Thread Makarius
https://isabelle.sketis.net/repos provides uniform repository clones of Isabelle + AFP -- this is updated via cron + ssh every 10min. The original motivation was to avoid recurrent oddities with https certificates from other repository servers, with the most recent incident for Bitbucket

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-04 Thread Makarius
On 04/02/2019 10:37, Lars Hupel wrote: > Is this related to the latest Poly/ML changes? The "slow" job still runs > on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware > is 8-core LRZ VM. I can confirm this: see

[isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-04 Thread Lars Hupel
Is this related to the latest Poly/ML changes? The "slow" job still runs on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware is 8-core LRZ VM. https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/1010/consoleFull ___