Dear Isabelle and AFP developers,
currently, isatest and afptest send build failure notifications to
specific people specified in a global list (isatest) or per entry
(afptest). How should this work in the future?
For isatest, I don't think this global list makes much sense. Rather
failures
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
> * archival of the build logs
As a temporary solution, I have now configured Jenkins to retain all
build logs. I've found some pointers how to make Jenkins store them into
some database, but will need to investigate further.
> * installing compilers and setting the various
>
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
> 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
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
> 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:
Hi Lars,
The theory Uint comes from Native_Word. I'll have a look and see whether this
can be fixed.
Andreas
On 31/01/16 22:21, Lars Hupel wrote:
* archival of the build logs
As a temporary solution, I have now configured Jenkins to retain all
build logs. I've found some pointers how to
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
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
10 matches
Mail list logo