On Mon, 14 Nov 2011, Johannes Hölzl wrote:
Am Montag, den 14.11.2011, 21:05 +0100 schrieb Alexander Krauss:
On 11/14/2011 08:43 PM, Johannes Hölzl wrote:
> Am Montag, den 14.11.2011, 19:27 +0100 schrieb Florian Haftmann:
>> Hi Johannes,
>>
>> two remarks:
>>
>> * http://isabelle.in.tum.de/reports/Isabelle/rev/e828ccc5c110
>>
>> With `notepad` you can prove everything without a trace in theory, which
>> eliminates the need for fiddling around with quick_and_dirty.
>
> I want to enforce that the user needs to activate quick_and_dirty in
> ROOT.ML, to remind him that there is something dirty.
This is rather non-standard and also breaks the test, cf.
http://isabelle.in.tum.de/reports/Isabelle/report/d6e6227d86634c02890a3e60e508abc3
(Tests are run without quick_and_dirty, and rightfully so.)
Oh, I didn't look at that. I removed the check now.
You really have to run a full "isabelle makeall all" before pushing
anything. Otherwise it wastes other people's time unnecessarily.
lemma "False" sorry is indeed a strange kind of markup...
Well False is proven anyway
You probably mean this one:
http://isabelle.in.tum.de/reports/Isabelle/diff/34d07cf7d207/src/HOL/Library/Code_Real_Approx_By_Float.thy#l1.139
That is a slightly different False theorem, since the kernel adds an
official oracle tag, which can be seen like this
...
lemma a: "False"
proof-
have "cos(pi/2) = 0" by(rule cos_pi_half)
moreover have "cos(pi/2) ≠ 0" by eval
ultimately show "False" by blast
qed
ML {* Thm.status_of @{thm a} *}
val it = {failed = false, oracle = true, unfinished = false}: {failed:
bool, oracle: bool, unfinished: bool}
ML {* Proofterm.all_oracles_of (Thm.proof_body_of @{thm a}) *}
val it = [("Code_Generator.holds_by_evaluation", Const ("dummy_pattern",
"_"))]: Proofterm.oracle list
Nonetheless, I agree with Florian that regular Library stuff should not
make it easy to get wrong oracular results.
and it is a easy check for quick_and_dirty.
That is actually not so easy. Since it is an old-style global reference
it depends on many side-conditions what it value is in a certain
situation. I still need to find ways to handle "session parameters" in a
robust manner. Old-style ROOT.ML is a bit too crude for that in the
general situation, i.e. interaction vs. batch mode.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
