[isabelle-dev] Isabelle/jEdit output panel
Here is an interesting update in Isabelle/cbcccf2a0f6f: at first sight there should be hardly any difference in the Output panel appearance and behaviour, but it is now based on completely different technology. The former Lobo/Cobra HTML4/CSS2 browser is no longer used, neither the new HTML5_Panel from JavaFX (which introduces its own complications). Instead, the existing semantic text rendering over regular jEdit text areas is applied to output as well. This is in the best tradition of Emacs, where "everything is a buffer". In Isabelle/jEdit almost everything is derived from TextArea, or better Rich_Text_Area. This also means that tooltips, hyperlinks etc. should now work the same for Output, just as for the input text. The next step will be to make tooltips and popups themselves use the same technology recursively. If something breaks down unexpectedly, because I've overlooking something important, the old HTML4 panel is still available as Output1 for the moment. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
On Fri, 21 Sep 2012, Tobias Nipkow wrote: This is just another reminder that people should watch the AFP when they check in changes, and fix them. The testboard runs most of the AFP. Once the testboard recovers, one could make this a bit more complete. I usually have FLYSPECK_SKIP_PROOFS=true in my settings and then run *all* of AFP in 35min on a plain-old 8-core workstation. The new Isabelle build configuration has the "condition" option to formalize the omission of theories, depending on given environment variables. ISABELLE_FULL_TEST (undefined by default) is already used as a convention to guard extra tests that take unusually long time. If ISABELLE_FULL_TEST would be checked instead of FLYSPECK_SKIP_PROOFS in afp/thys/Flyspeck-Tame/ArchComp.thy with the inverted meaning, then one could discontinue the AFP vs. AFP_big distinction. It would work for everyone by default within the range of 0.5 .. 2h total. The full test would then be run infrequently by one of the standard test frameworks in the background. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
On Fri, 21 Sep 2012, Jasmin Christian Blanchette wrote: Am 21.09.2012 um 09:18 schrieb Tobias Nipkow: The testboard runs most of the AFP. For the last three days, neither the tests nor testboard have been working. http://isabelle.in.tum.de/reports/Isabelle http://isabelle.in.tum.de/testboard/Isabelle For me there is still some dark matter here that I don't understand. The totality of Mira configuration is difficult to see. Without looking, I suspect that the update to polyml-5.5.0 Isabelle/617869cd779c confuses Mira, which still has some odd references to the old /home/isabelle/contrib_devel with its funny symlinks. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
I am just at the moment trying to get it running again. Lukas On 09/21/2012 10:54 AM, Jasmin Christian Blanchette wrote: Am 21.09.2012 um 09:18 schrieb Tobias Nipkow: The testboard runs most of the AFP. For the last three days, neither the tests nor testboard have been working. http://isabelle.in.tum.de/reports/Isabelle http://isabelle.in.tum.de/testboard/Isabelle Jasmin ___ 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] Fwd: status (AFP)
Am 21.09.2012 um 09:18 schrieb Tobias Nipkow: > The testboard runs most of the AFP. For the last three days, neither the tests nor testboard have been working. http://isabelle.in.tum.de/reports/Isabelle http://isabelle.in.tum.de/testboard/Isabelle Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
That's very kind of him, assuming he was not the one who broke KBPs. This is just another reminder that people should watch the AFP when they check in changes, and fix them. The testboard runs most of the AFP. Tobias Am 21/09/2012 09:12, schrieb Lukas Bulwahn: > Thanks to Dmitriy's effort, all AFP entries run successfully again. > > > Original Message > Subject: status (AFP) > Date: Fri, 21 Sep 2012 09:10:43 +0200 (CEST) > From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle ) > To: undisclosed-recipients:; > > > > The status of the following AFP entries changed or remains FAIL: > [KBPs] changed from FAIL to ok. > > Full entry status at http://afp.sourceforge.net/status.shtml > > AFP version: development -- hg id c3a75d6d802a > Isabelle version: devel -- hg id 7bb0d515ccbc > Test ended on: macbroy2, Fri Sep 21 09:10:43 CEST 2012. > > Have a nice day, > isatest > > > > > This body part will be downloaded on demand. > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Fwd: status (AFP)
Thanks to Dmitriy's effort, all AFP entries run successfully again. Original Message Subject:status (AFP) Date: Fri, 21 Sep 2012 09:10:43 +0200 (CEST) From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle ) To: undisclosed-recipients:; The status of the following AFP entries changed or remains FAIL: [KBPs] changed from FAIL to ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id c3a75d6d802a Isabelle version: devel -- hg id 7bb0d515ccbc Test ended on: macbroy2, Fri Sep 21 09:10:43 CEST 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 FunWithFunctions: ok Coinductive: ok 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 Example-Submission: ok SumSquares: ok BDD: ok JiveDataStoreModel: 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 HRB-Slicing: ok DPT-SAT-Solver: ok RIPEMD-160-SPARK: ok Flyspeck-Tame: ok Regular-Sets: ok RSAPSS: ok LightweightJava: ok Gauss-Jordan-Elim-Fun: ok 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 FunWithTilings: ok SenSocialChoice: ok CCS: 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 Slicing: 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 Fri Sep 21 06:31:44 CEST 2012, macbroy2 begin hg pull/update pulling from ssh://isat...@afp.hg.sourceforge.net/hgroot/afp/afp searching for changes adding changesets adding manifests adding file changes added 1 changesets with 1 changes to 1 files 1 files updated, 0 files merged, 0 files removed, 0 files unresolved remote: Running preoutgoing hook remote: Use of uninitialized value in concatenation (.) or string at /etc/mercurial/preoutgoing line 36. end hg pull/update AFP version: development -- hg id c3a75d6d802a Isabelle version: devel -- hg id 7bb0d515ccbc Building HOLCF ... Finished HOLCF (0:00:50 elapsed time, 0:01:01 cpu time, factor 1.22) Building HOL-Nominal ... Finished HOL-Nominal (0:00:21 elapsed time, 0:00:23 cpu time, factor 1.09) Building HOL-Multivariate_Analysis ... Finished HOL-Multivariate_Analysis (0:03:00 elapsed time, 0:06:32 cpu time, factor 2.17) Building HOL-Word ... Finished HOL-Word (0:00:38 elapsed time, 0:01:07 cpu time, factor 1.76) Building Jinja ... Finished Jinja (0:05:48 elapsed time, 0:13:16 cpu time, factor 2.28) Building LatticeProperties ... Finished LatticeProperties (0:00:20 elapsed time, 0:00:22 cpu time, factor 1.10) Building HOL-Probability ... Finished HOL-Probability (0:01:43 elapsed time, 0:03:24 cpu time, factor 1.98) Building Group-Ring-Module ... Finished Group-Ring-Module (0:03:22 elapsed time, 0:07:08 cpu time, factor 2.11) Building Simpl ... Finished Simpl (0:02:35 elapsed time, 0:04:55 cpu time, factor 1.90) Building Collections ... Finished Collections (0:05:32 elapsed time, 0:08:31 cpu time, factor 1.53) Building Refine_Monadic ... Finished Refine_Monadic (0:01:51 elapsed time, 0:02:51 cpu time, factor 1.54) Building List-Infinite ... Finished List-Infinite (0:00:45 elapsed time, 0:01:18 cpu time, factor 1.73) Building Nat-Interval-Logic ... Finished Nat-Interval-Logic (0:00:50 elapsed time, 0:01:19 cpu time, factor 1.58) Running Flyspeck-Tame ... Finished Flyspeck-Tame (0:03:12 elapsed time, 0:06:10 cpu time, factor 1.92) Running JinjaThreads ... Finished JinjaThreads (0:57:08 elapsed time, 1:51:07 cpu time, factor 1.94) Running HRB-Slicing ... Finished HRB-Slicing (0:05:54
