On 02/11/16 15:58, Lawrence Paulson wrote: > I have to say, I’m absolutely mystified by the response to my suggestion.
Why? I did not reject the idea, but only put it into the context of Isabelle. MetiTarski is a small research experiment, but Isabelle a huge and complex software product, with very high standards. > We have spent a lot of time discussing problems caused by the cost of > regression testing, and now we have the possibility of reducing that by 30%. Where is the empirical measurement for Isabelle? Without that it is just speculation. A quick test with x86_64 and int = FixedInt might actually give some ideas about the order of potential performance improvement. Do you want to make one? In the Jenkins project, there were also proposals to move to 64bit by default, and thus lose a lot of performance. (The general waste of resources of Jenkins is caused by high-level policies, though, and theses were not openly discussed so far.) > As to changes in behaviour that could be caused by overflows, I checked: > exception Overflow is explicitly caught in only two places throughout > the sources, both in HOL decision procedures (and therefore well outside > the kernel) while the wildcard exception is caught in three places in > Pure. I routinely check these things before each release. Catch-all patterns are more frequent than that, but they are OK. I don't think that such a change would cause wrong results, but just unexpected failure, and that is already bad enough in everyday use. > No exception handlers had to be added when I converted MetiTarski > to use fixed integers. An uncaught exception doesn’t prove anything, of > course. BTW, you have a lot of catch-all exception handlers in MetiTarski. The Isabelle/ML IDE shows that -- my changeset from last summer is attached again. Makarius
# HG changeset patch # User wenzelm # Date 1464704221 -7200 # Tue May 31 16:17:01 2016 +0200 # Node ID e517f280847f40ff7b3a104c4c0f46bca815cc54 # Parent b11e8139b880bde17d291e1d35c3a3577185a82f basic setup for Isabelle/SML IDE; diff -r b11e8139b880 -r e517f280847f src/+ld.sml --- a/src/+ld.sml Mon Mar 30 15:28:39 2015 +0100 +++ b/src/+ld.sml Tue May 31 16:17:01 2016 +0200 @@ -66,7 +66,12 @@ use"Tptp.sig"; use"Tptp.sml"; use"SMTLIB.sig"; use"SMTLIB.sml"; -use"Syntax/load.sml"; +use"Syntax/lib/base.sig"; +use"Syntax/lib/join.sml"; +use"Syntax/lib/lrtable.sml"; +use"Syntax/lib/stream.sml"; +use"Syntax/lib/parser2.sml"; +use"Syntax/load0.sml"; use"Options.sig"; use"Options.sml"; use"metis.sml"; diff -r b11e8139b880 -r e517f280847f src/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ROOT.ML Tue May 31 16:17:01 2016 +0200 @@ -0,0 +1,75 @@ +SML_file "Portable.sig"; +SML_file "Random.sig"; SML_file "Random.sml"; +SML_file "PortablePolyml.sml"; +SML_file "Polyhash.sig"; SML_file "Polyhash.sml"; +SML_file "Useful.sig"; SML_file "Useful.sml"; +SML_file "rat.sml"; (*John Harrison's code*) +SML_file "Lazy.sig"; SML_file "Lazy.sml"; +SML_file "Map.sig"; SML_file "Map.sml"; +SML_file "Set.sig"; SML_file "Set.sml"; +SML_file "Ordered.sig"; SML_file "Ordered.sml"; +SML_file "KeyMap.sig"; SML_file "KeyMap.sml"; +SML_file "ElementSet.sig"; SML_file "ElementSet.sml"; +SML_file "Sharing.sig"; SML_file "Sharing.sml"; +SML_file "Stream.sig"; SML_file "Stream.sml"; +SML_file "Heap.sig"; SML_file "Heap.sml"; +SML_file "Print.sig"; SML_file "Print.sml"; +SML_file "Parse.sig"; SML_file "Parse.sml"; +SML_file "Name.sig"; SML_file "Name.sml"; +SML_file "NameArity.sig"; SML_file "NameArity.sml"; +SML_file "Term.sig"; SML_file "Term.sml"; +SML_file "Subst.sig"; SML_file "Subst.sml"; +SML_file "Atom.sig"; SML_file "Atom.sml"; +SML_file "Formula.sig"; SML_file "Formula.sml"; +SML_file "Literal.sig"; SML_file "Literal.sml"; +SML_file "KnuthBendixOrder.sig"; SML_file "KnuthBendixOrder.sml"; +SML_file "Poly.sig"; SML_file "Poly.sml"; +SML_file "RCF/Common.sig"; SML_file "RCF/Common.sml"; +SML_file "RCF/Algebra.sig"; SML_file "RCF/Algebra.sml"; +SML_file "RCF/Groebner.sig"; SML_file "RCF/Groebner.sml"; +SML_file "RCF/SMT.sig"; SML_file "RCF/SMT.sml"; +SML_file "RCF/IntvlsFP.sig"; SML_file "RCF/IntvlsFP.sml"; +SML_file "RCF/Resultant.sig"; SML_file "RCF/Resultant.sml"; +SML_file "RCF/Sturm.sig"; SML_file "RCF/Sturm.sml"; +SML_file "RCF/RealAlg.sig"; SML_file "RCF/RealAlg.sml"; +SML_file "RCF/MTAlgebra.sig"; SML_file "RCF/MTAlgebra.sml"; +SML_file "RCF/CADProjO.sig"; SML_file "RCF/CADProjO.sml"; +SML_file "RCF/Mathematica.sig"; SML_file "RCF/Mathematica.sml"; +SML_file "RCF/Qepcad.sig"; SML_file "RCF/Qepcad.sml"; +SML_file "RCF/Nullsatz.sig"; SML_file "RCF/Nullsatz.sml"; +SML_file "RCF/CertRCFk.sig"; SML_file "RCF/CertRCFk.sml"; +SML_file "RCF/CertRCFp.sig"; SML_file "RCF/CertRCFp.sml"; +SML_file "RCF/RCF.sig"; SML_file "RCF/RCF.sml"; +SML_file "Thm.sig"; SML_file "Thm.sml"; +SML_file "Proof.sig"; SML_file "Proof.sml"; +SML_file "Rule.sig"; SML_file "Rule.sml"; +SML_file "Normalize.sig"; SML_file "Normalize.sml"; +SML_file "Model.sig"; SML_file "Model.sml"; +SML_file "Problem.sig"; SML_file "Problem.sml"; +SML_file "TermNet.sig"; SML_file "TermNet.sml"; +SML_file "AtomNet.sig"; SML_file "AtomNet.sml"; +SML_file "LiteralNet.sig"; SML_file "LiteralNet.sml"; +SML_file "Subsume.sig"; SML_file "Subsume.sml"; +SML_file "Rewrite.sig"; SML_file "Rewrite.sml"; +SML_file "Units.sig"; SML_file "Units.sml"; +SML_file "Clause.sig"; SML_file "Clause.sml"; +SML_file "Active.sig"; SML_file "Active.sml"; +SML_file "Waiting.sig"; SML_file "Waiting.sml"; +SML_file "SplitStack.sig"; SML_file "SplitStack.sml"; +SML_file "Resolution.sig"; SML_file "Resolution.sml"; +SML_file "Tptp.sig"; SML_file "Tptp.sml"; +SML_file "SMTLIB.sig"; SML_file "SMTLIB.sml"; + +SML_file "Syntax/lib/base.sig"; +SML_file "Syntax/lib/join.sml"; +SML_file "Syntax/lib/lrtable.sml"; +SML_file "Syntax/lib/stream.sml"; +SML_file "Syntax/lib/parser2.sml"; +SML_file "Syntax/load0.sml"; +SML_file "Syntax/mt.grm.sig"; +SML_file "Syntax/mt.grm.sml"; +SML_file "Syntax/mt.lex.sml"; +SML_file "Syntax/load.sml"; + +SML_file "Options.sig"; SML_file "Options.sml"; +SML_file "metis.sml"; diff -r b11e8139b880 -r e517f280847f src/Syntax/load.sml --- a/src/Syntax/load.sml Mon Mar 30 15:28:39 2015 +0100 +++ b/src/Syntax/load.sml Tue May 31 16:17:01 2016 +0200 @@ -1,40 +1,3 @@ -use"Syntax/lib/base.sig"; -use"Syntax/lib/join.sml"; -use"Syntax/lib/lrtable.sml"; -use"Syntax/lib/stream.sml"; -use"Syntax/lib/parser2.sml"; - -fun goodAtom (Term.Fn (s,_)) = size s > 0 andalso Char.isLower (String.sub (s,0)) - | goodAtom _ = false; - -fun fmOfAtom t = - Formula.Atom (if goodAtom t then Term.destFn t else ("Bad_Formula",[t])); - -fun termOfDecimal s = - let val mant::rest = String.tokens (fn c => c = #"e" orelse c = #"E") s (*remove exponent*) - val e = Option.valOf (IntInf.fromString (hd rest)) handle Empty => 0 - val tenexp = Rat.exp (Rat.rat_of_intinf 10, Rat.rat_of_intinf e) - val [uns] = String.tokens (fn c => c = #"+" orelse c = #"-") mant (*remove sign*) - val a::ss = String.fields (fn c => c = #".") uns (*integer part*) - val b = hd ss handle Empty => "" - val n = String.size b - val i = (if a="" then 0 else Option.valOf (IntInf.fromString a)) - val j = (if b="" then 0 else Option.valOf (IntInf.fromString b)) - val tenn = Useful.exp IntInf.* 10 n 1 - val r = Rat.mult (tenexp, Rat.rat_of_quotient (i*tenn+j, tenn)) - in Term.Rat (if String.isPrefix "-" s then Rat.neg r else r) end - handle _ => (print ("Unable to translate numeric constant " ^ s ^ "\n"); - raise Parse.NoParse); - -fun litOfInterval (x, (il,lower,iu,upper)) = - (true, ("interval", - [Term.Rat (Rat.rat_of_int il), lower, - Term.Rat (Rat.rat_of_int iu), upper, x])); - -use"Syntax/mt.grm.sig"; -use"Syntax/mt.grm.sml"; -use"Syntax/mt.lex.sml"; - structure MTLrVals : MT_LRVALS = MTLrValsFun(structure Token = LrParser.Token); diff -r b11e8139b880 -r e517f280847f src/Syntax/load0.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Syntax/load0.sml Tue May 31 16:17:01 2016 +0200 @@ -0,0 +1,26 @@ +fun goodAtom (Term.Fn (s,_)) = size s > 0 andalso Char.isLower (String.sub (s,0)) + | goodAtom _ = false; + +fun fmOfAtom t = + Formula.Atom (if goodAtom t then Term.destFn t else ("Bad_Formula",[t])); + +fun termOfDecimal s = + let val mant::rest = String.tokens (fn c => c = #"e" orelse c = #"E") s (*remove exponent*) + val e = Option.valOf (IntInf.fromString (hd rest)) handle Empty => 0 + val tenexp = Rat.exp (Rat.rat_of_intinf 10, Rat.rat_of_intinf e) + val [uns] = String.tokens (fn c => c = #"+" orelse c = #"-") mant (*remove sign*) + val a::ss = String.fields (fn c => c = #".") uns (*integer part*) + val b = hd ss handle Empty => "" + val n = String.size b + val i = (if a="" then 0 else Option.valOf (IntInf.fromString a)) + val j = (if b="" then 0 else Option.valOf (IntInf.fromString b)) + val tenn = Useful.exp IntInf.* 10 n 1 + val r = Rat.mult (tenexp, Rat.rat_of_quotient (i*tenn+j, tenn)) + in Term.Rat (if String.isPrefix "-" s then Rat.neg r else r) end + handle _ => (print ("Unable to translate numeric constant " ^ s ^ "\n"); + raise Parse.NoParse); + +fun litOfInterval (x, (il,lower,iu,upper)) = + (true, ("interval", + [Term.Rat (Rat.rat_of_int il), lower, + Term.Rat (Rat.rat_of_int iu), upper, x]));
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev