Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

> I have now done this in Isabelle/705d4c4003ea. > > It means that ISABELLE_FULL_TEST no longer occurs in the main Isabelle > repository. The extra slow sessions are in ~~/src/Benchmarks, and only > tested by special background jobs that take care of that. (Presently none!) Thanks. I will add a

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

On Wed, 3 Feb 2016, Jasmin Blanchette wrote: I have a slight worry concerning the characterization and naming as "benchmarks". From what I understand, a "benchmark" is a theory file that tests the performance of the system. I have introduced this terminology many years ago. The idea is that

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

> What is special about Sudoku? You're right, probably nothing. >> SMT_Tests (requires Z3) > ... > In 2013 we did not have Z3 as default component, usable for everybody. Now > the condition on it is always true -- z3 is always enabled. We could indeed enable it by default. >> Slow: >> Brackin

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

>> What remains are various benchmarks. We could move these sessions to >> ~~/src/Benchmarks and omit that directory in ~~/ROOTS. Thus it can be >> included on demand like this: >> >> isabelle build -d '~~/src/Benchmarks' -a >> >> or like this: >> >> isabelle build -D '~~/src/Benchmarks' >>

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

> What remains are various benchmarks. We could move these sessions to > ~~/src/Benchmarks and omit that directory in ~~/ROOTS. Thus it can be > included on demand like this: > > isabelle build -d '~~/src/Benchmarks' -a > > or like this: > > isabelle build -D '~~/src/Benchmarks' > > This

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

On Sun, 31 Jan 2016, Lars Hupel wrote: The "ISABELLE_FULL_TEST" variable and "slow" group are somehow adhoc measures to get meaningful interactive tests, without wasting too much time. It probably makes sense to imitate that for "testboard" setups. The idea is to distribute the build load

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

Maybe it’s time. They’ve not made it better, and it seems pretty hopeless now. Larry > On 31 Jan 2016, at 13:41, Makarius wrote: > > We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session for > SML/NJ. > > Or we could discontinue SML/NJ altogether. I

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

> The "ISABELLE_FULL_TEST" variable and "slow" group are somehow adhoc > measures to get meaningful interactive tests, without wasting too much > time. It probably makes sense to imitate that for "testboard" setups. The idea is to distribute the build load over multiple machines, since that

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

On Sun, 31 Jan 2016, Lars Hupel wrote: unexpected exception (bug?) in SML/NJ: Io [Io: openIn failed on "/build/smlnj-tOOpSy/smlnj-110.76/sml.boot.x86-unix/smlnj/basis/.cm/x86-unix/basis.cm", No such file or directory] raised at: Basis/Implementation/IO/bin-io-fn.sml:617.25-617.71

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

> Building with SML/NJ configuration is trivial. It would be "just another > job" in Jenkins. I'd just need to know about what to build precisely. > Can you explain to me what the ML_SYSTEM_POLYML variable means? I was speaking too early. Here's what I get when trying to build Pure with SML/NJ:

[isabelle-dev] Grouping ISABELLE_FULL_TEST?

As of 527488dc8b90, there are five sessions which contain theories that are only processed under ISABELLE_FULL_TEST=true: HOL-ex Sudoku HOL-Datatype_Examples Brackin IsaFoR Misc_N2M HOL-Word-SMT_Examples SMT_Tests HOL-Quickcheck_Benchmark Find_Unused_Assms_Examples

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

On Sun, 31 Jan 2016, Lars Hupel wrote: As of 527488dc8b90, there are five sessions which contain theories that are only processed under ISABELLE_FULL_TEST=true: HOL-ex Sudoku HOL-Datatype_Examples Brackin IsaFoR Misc_N2M HOL-Word-SMT_Examples SMT_Tests HOL-Quickcheck_Benchmark