Re: [isabelle-dev] AFP devel broken

[Gerwin Klein]

It now finally works again.

The problem embarrassingly was that we forgot to add the entry to the list of 
sessions in thys/ROOTS. We should probably generate that file automatically in 
the future for AFP.

Cheers,
Gerwin

On 29/11/2012, at 11:47 PM, Christian Sternagel  wrote:

> On 11/09/2012 12:26 AM, Christian Sternagel wrote:
>> Just follow the "Browse theories" link of any devel entry, e.g.,
>> http://afp.sourceforge.net/browser_info/devel/HOL/Bondy/index.html
> As far as I can tell the problem still remains. Is it known in the meantime 
> what the problem is?
> 
> cheers
> 
> chris
> ___
> 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

[isabelle-dev] Fwd: status (AFP)

[Gerwin Klein]

The afp test is now back to normal operation and the devel website update is 
working again as well.

The two below are real failures, possibly have been there for a while masked by 
the problems the test had.

Cheers,
Gerwin

Begin forwarded message:

> From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle )
> Subject: status (AFP)
> Date: 16 December 2012 5:59:14 PM AEDT
> To: undisclosed-recipients:;
> 
> The status of the following AFP entries changed or remains FAIL: 
> [Possibilistic_Noninterference] is still on FAIL.
> [Separation_Logic_Imperative_HOL] is still on FAIL.
> 
> Full entry status at http://afp.sourceforge.net/status.shtml
> 
> AFP version: development -- hg id 519e8aa3ea9f
> Isabelle version: devel -- hg id e4dc37ec1427
> Test ended on: macbroy2, Sun Dec 16 07:59:14 CET 2012.
> 
> Have a nice day,
>  isatest
> 
Stream-Fusion: ok
Ramsey-Infinite: ok
Binomial-Heaps: ok
Ordinals_and_Cardinals: ok
ClockSynchInst: ok
Huffman: ok
Completeness: ok
Well_Quasi_Orders: ok
Abstract-Hoare-Logics: ok
Free-Boolean-Algebra: ok
Stuttering_Equivalence: ok
Girth_Chromatic: ok
Valuation: ok
InformationFlowSlicing_Intra: ok
FunWithFunctions: ok
Coinductive: ok
Possibilistic_Noninterference: FAIL
Heard_Of: ok
Abstract-Rewriting: ok
Matrix: ok
POPLmark-deBruijn: ok
MonoBoolTranAlgebra: ok
FeatherweightJava: ok
DiskPaxos: ok
Free-Groups: ok
Functional-Automata: ok
GraphMarkingIBP: ok
Transitive-Closure-II: ok
Tycon: ok
BytecodeLogicJmlTypes: ok
Finger-Trees: ok
WorkerWrapper: ok
Separation_Algebra: ok
General-Triangle: ok
Program-Conflict-Analysis: ok
LinearQuantifierElim: ok
GenClock: ok
Inductive_Confidentiality: ok
Recursion-Theory-I: ok
Efficient-Mergesort: ok
BinarySearchTree: ok
TLA: ok
Lam-ml-Normalization: ok
CoreC++: ok
Marriage: ok
Shivers-CFA: ok
SATSolverVerification: ok
InformationFlowSlicing_Inter: ok
Example-Submission: ok
SumSquares: ok
JiveDataStoreModel: ok
BDD: ok
Polynomials: ok
Datatype_Order_Generator: ok
Verified-Prover: ok
Topology: ok
KBPs: ok
ArrowImpossibilityGS: ok
Lazy-Lists-II: ok
Locally-Nameless-Sigma: ok
DataRefinementIBP: ok
JinjaThreads: ok
DPT-SAT-Solver: ok
Tarskis_Geometry: ok
RIPEMD-160-SPARK: ok
Flyspeck-Tame: ok
Regular-Sets: ok
RSAPSS: ok
LightweightJava: ok
Gauss-Jordan-Elim-Fun: ok
Separation_Logic_Imperative_HOL: FAIL
AVL-Trees: ok
Category: ok
AutoFocus-Stream: ok
CofGroups: ok
Perfect-Number-Thm: ok
Depth-First-Search: ok
Abortable_Linearizable_Modules: ok
Statecharts: ok
PseudoHoops: ok
Max-Card-Matching: ok
Bondy: ok
FunWithTilings: ok
SenSocialChoice: ok
CCS: ok
Open_Induction: ok
List-Index: ok
Markov_Models: ok
Cauchy: ok
Ordinal: ok
Myhill-Nerode: ok
Binomial-Queues: ok
Fermat3_4: ok
FOL-Fitting: ok
MuchAdoAboutTwo: ok
Dijkstra_Shortest_Path: ok
SIFPL: ok
Presburger-Automata: ok
Circus: ok
Transitive-Closure: ok
Impossible_Geometry: ok
Category2: ok
Integration: ok
MiniML: ok
NormByEval: ok
PCF: ok
SequentInvertibility: ok
Pi_Calculus: ok
FileRefinement: ok
FFT: ok
Robbins-Conjecture: ok
Compiling-Exceptions-Correctly: ok
Ordinary_Differential_Equations: ok
VolpanoSmith: ok
HotelKeyCards: ok
Tree-Automata: ok
FinFun: ok
Psi_Calculi: ok
Lower_Semicontinuous: ok
Start test for /home/isatest/afp/devel at Sun Dec 16 06:05:45 CET 2012, macbroy2

begin hg pull/update
pulling from ssh://isat...@afp.hg.sourceforge.net/hgroot/afp/afp
searching for changes
no changes found
end hg pull/update

AFP version: development -- hg id 519e8aa3ea9f
Isabelle version: devel -- hg id e4dc37ec1427

Building HOLCF ...
Finished HOLCF (0:00:36 elapsed time, 0:00:58 cpu time, factor 1.61)
Building HOL-Nominal ...
Finished HOL-Nominal (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.57)
Building HOL-Multivariate_Analysis ...
Finished HOL-Multivariate_Analysis (0:01:54 elapsed time, 0:05:14 cpu time, 
factor 2.75)
Building HOL-Word ...
Finished HOL-Word (0:00:28 elapsed time, 0:01:02 cpu time, factor 2.21)
Building Jinja ...
Finished Jinja (0:04:02 elapsed time, 0:12:23 cpu time, factor 3.07)
Building LatticeProperties ...
Finished LatticeProperties (0:00:14 elapsed time, 0:00:21 cpu time, factor 1.50)
Building HOL-Probability ...
Finished HOL-Probability (0:01:30 elapsed time, 0:04:08 cpu time, factor 2.75)
Building HRB-Slicing ...
Finished HRB-Slicing (0:04:57 elapsed time, 0:15:15 cpu time, factor 3.08)
Building Slicing ...
Finished Slicing (0:04:43 elapsed time, 0:15:04 cpu time, factor 3.19)
Building Group-Ring-Module ...
Finished Group-Ring-Module (0:02:17 elapsed time, 0:06:49 cpu time, factor 2.98)
Building Simpl ...
Finished Simpl (0:01:42 elapsed time, 0:04:49 cpu time, factor 2.83)
Building Collections ...
Finished Collections (0:04:00 elapsed time, 0:09:28 cpu time, factor 2.36)
Building Refine_Monadic ...
Finished Refine_Monadic (0:01:05 elapsed time, 0:02:29 cpu time, factor 2.29)
Building List-Infinite ...
Finished List-Infinite (0:00:32 elapsed time, 0:01:10 cpu time, factor 2.18)
Building Nat-Interval-Logic ...
Finished Nat-Interval-Logic (0:00:34 elapsed time, 0:

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

[Lukas Bulwahn]

On 12/11/2012 10:27 PM, Makarius wrote:

On Mon, 10 Dec 2012, Makarius wrote:


On Fri, 30 Nov 2012, Lukas Bulwahn wrote:

It must be considered unmaintained. The benchmarks themself I will 
irregularly have time on weekends and nights to have a look, but I 
cannot keep up with "Isabelle roaring ahead".


After several weeks of isatest failing on HOL-Quickcheck_Benchmark 
(now at least reliably with Interrupt, not Timeout), the situation is 
still unchanged in the repository (presently 0a740d127187).


In Isabelle/d466ebc27810 isatest is silenced for now, to give Lukas a 
window of opportunity to make up his mind.  Note that src/HOL/ROOT has 
other quickcheck tests commented out for a long time already.


If nothing happens, lets say until the last week of the year, I will 
start moving find_unused_assms to HOL/ex.


Things have changed in 768a3fbe4149 and it solved the issue in 
find_unused_assms.


Just for your information, it was due to a non-terminating code equation 
for the vimage constant.
The Codegenerator_Test session only checks if code is generated but not 
if the executable equations make much sense, the find_unused_assm theory 
complements that by actually executing a number of generated programs 
and should not be dropped in the future if it ever breaks again. A 
failure in this theory indicates some open issue in the code generation 
process or setup.


If other problems occur, I am willing to help whenever I can. However as 
I left Garching, it takes some time to address those issues.
Makarius, thanks for your patience and your work bisecting the cause of 
the failure.


Lukas


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

[Lukas Bulwahn]

On 12/11/2012 10:27 PM, Makarius wrote:

On Mon, 10 Dec 2012, Makarius wrote:


On Fri, 30 Nov 2012, Lukas Bulwahn wrote:

It must be considered unmaintained. The benchmarks themself I will 
irregularly have time on weekends and nights to have a look, but I 
cannot keep up with "Isabelle roaring ahead".


After several weeks of isatest failing on HOL-Quickcheck_Benchmark 
(now at least reliably with Interrupt, not Timeout), the situation is 
still unchanged in the repository (presently 0a740d127187).


In Isabelle/d466ebc27810 isatest is silenced for now, to give Lukas a 
window of opportunity to make up his mind.  Note that src/HOL/ROOT has 
other quickcheck tests commented out for a long time already.


If nothing happens, lets say until the last week of the year, I will 
start moving find_unused_assms to HOL/ex.


Things have changed in 768a3fbe4149 and it solved the issue in 
find_unused_assms.


Just for your information, it was due to a non-terminating code equation 
for the vimage constant.
The Codegenerator_Test session only checks if code is generated but not 
if the executable equations make much sense, the find_unused_assm theory 
complements that by actually executing a number of generated programs 
and should not be dropped in the future if it ever breaks again. A 
failure in this theory indicates some open issue in the code generation 
process or setup.


If other problems occur, I am willing to help whenever I can. However as 
I left Garching, it takes some time to address those issues.
Makarius, thanks for your patience and your work bisecting the cause of 
the failure.


Lukas


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev