Hi all,
again a report about the current affairs:
a) state of discussion
IMHO I view the discussion at the point that we want 'a set back after
the next release. As a consequence, developers are cordially invited to
figure out remaining problems involving their contributions to the
system, or scream aloud when their resources do not allow so at the moment.
b) state of affairs in the distribution
failing:
HOL-ex FAILED
-> figure out problem with »refute« in Refute_Examples.thy with
"distinct [a, b]"
-> two proofs commented out, would need to enter the game of
proof-text minimazation
HOL-Nominal-Examples FAILED
-> still existing user-space problem, I will look after it
HOL-Metis_Examples FAILED
HOL-MicroJava FAILED
-> user-space problem, should be easy to solve
HOL-Nitpick_Examples FAILED
HOL-Predicate_Compile_Examples FAILED
HOL-Word-SMT_Examples FAILED
HOL-TPTP FAILED
HOL-IMP FAILED
-> codegen problem, I will look after it
working, but needs improvement:
HOL-ex FAILED
-> two proofs in Set_Theory commented out, would need to enter the
game of proof-text minimazation
HOLCF
-> type class instantiation for sets needed, c.f. ->
http://isabelle.in.tum.de/reports/Isabelle/rev/535290c908ae
c) state of affairs in the AFP
currently failing (including transitive failures):
BDD Cauchy Coinductive Collections Completeness CoreC++
DataRefinementIBP FinFun Free-Groups Functional-Automata GraphMarkingIBP
HRB-Slicing InformationFlowSlicing Jinja LightweightJava
LinearQuantifierElim Ordinals_and_Cardinals POPLmark-deBruijn
Regular-Sets Shivers-CFA Simpl Slicing Tree-Automata
I.e 23 out of 99, which does not look that bad. I guess most of these
sessions have come into being after Isabelle2008.
It would be a bad idea to go ahead and provide forked versions of these.
Better:
* Figure out where the problem is, maybe with some experiments.
* Contact the author and ask what (s)he thinks about that.
* Some things have already been reported to be repaired by a change in a
distribution theory rather than the AFP application.
Maybe good starting points are sessions whose contributors are also
developers.
d) enivsaged working plan
1.
* go on with activities from above
* (maybe)
hide_fact (open) Set.mem_def Set.Collect_def
to indicate that something is going on with these
2. RELEASE
3. introduce set type constructor
* backport necessary changes (as little invasive as possible) from
isabelle_set
* add naive code generator setup for sets in Set.thy (using set ::
'a list => 'a set)
* instantiation set :: ("{random, type}") random
* drop theory Executable_Set
* drop optional special type alias treatment in Pure/Isar/code.ML
(Florian)
* drop theory CSet (naive version, maybe not quotient version)
* restore previous rule declarations:
* lemma predicate1I [Pure.intro!, intro!]
* lemma pred_equals_eq [pred_set_conv]
* lemma pred_subset_eq [pred_set_conv]
* mark _apply rules for pointwise operations on functions as [simp]
* provide theories Dlist_Set, RBT_Set (or maybe Mapping_Set), etc.
* backport Set_Algebras to type classes
e) References:
Isabelle patched:
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set
AFP patched: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/afp_set
(although its there, we should avoid using it)
The historical critical changesets:
http://isabelle.in.tum.de/reports/Isabelle/shortlog/d889d57445dc
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
