Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML
This fix solves the problem with the exception. I tried it with 574613b47583. Can you add it to the repository as I do not have wirte access to that. Thanks, Andreas Lawrence Paulson schrieb: Thank you for looking there! This is the most plausible culprit. But it is strange that this problem has arisen before. A possible fix is to replace the last line of the function timing_depth_tac in that file as follows: handle PROVE = Seq.empty | THM _ = Seq.empty; Andreas, do you want to try this and see if it helps? Larry On 27 May 2011, at 15:27, Stefan Berghofer wrote: Hi Larry and Andreas, there is another occurrence of gconv_rule in Provers/blast.ML (in function timing_depth_tac). Since the exception is thrown when invoking blast, this occurrence of gconv_rule may be the culprit. -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New Testing Infrastructure -- status report
Awesome! It looks positively industrial in scale. Larry On 30 May 2011, at 08:54, Alexander Krauss wrote: Hi all, In the past weeks, there has been some progress with our new testing infrastructure, which I would like to summarize here. Please give feedback, ask questions, and discuss. Really fast status for isabelle makeall = Thanks to a new fat server with 24 cores and 130G of RAM, we can now run isabelle makeall all in 17-18 minutes. This is done on all changesets as they come in, so we always know quickly when the tip of the repository breaks. The reports with logs etc. can all be browsed at http://isabelle.in.tum.de/reports/Isabelle/ This is a fully functional repository view, annotated with test results. The first column of flashlights represents the status of Isabelle_makeall. Developer-initiated tests = Apart from changesets from the official repository, the system also considers changesets from a special testboard repository. All developers can push their untested changes here, to get some automatic feedback. Try it out, it is really convenient. To use testboard, it is convenient to add the following to your ~/.hgrc [paths] testboard = ssh://usern...@macbroy20.informatik.tu-muenchen.de//home/isabelle-repository/repos/testboard Then, local changes can be pushed to testboard via hg push -f testboard and will usually be considered fairly quickly by the scheduler. (Note: -f is required, since the testboard repository will usually have multiple heads. Never use -f when pushing to the main development repository!) The reports from testboard can be viewed at http://isabelle.in.tum.de/testboard/Isabelle Note that testboard should be considered write-only. You should never pull from it unless you want to get everybody's unfinished stuff! SML/NJ testing == Building the HOL image takes ca. 3-4 hours, and a full makeall takes ca. 24 hours. This has been prohibitive for pre-push testing with SML/NJ, so people generally have fixed issues after getting a failure. The new setup supports the same style of working but gives quicker feedback. Both the HOL image and makeall are run continuously, so there is much quicker feedback. The third column in the reports view signals the status of SML/NJ builds. Note that the SML_makeall test still excludes a small number of sessions which are too big to fit into memory. AFP === Currently, there is a reduced build of the AFP, which is run continuously, but it still excludes Flyspeck_Tame and JinjaThreads. When Gerwin is here, we'll try to make this build equivalent to the official AFP builds. The results are signalled in the second column in the reports view. Data collection === Performance data is collected in every run. When Makarius is available again, we must decide on a set of sessions to be run regularly in a reproducible environment (i.e., without other jobs or interactive activity on the same machine), to get less fluctuation in the measurements. Judgement Day benchmarks are now run continuously on two lxlabbroy machines. This is still somewhat preliminary, and I must coordinate with Jasmin and Sascha what data should best be collected and how. Mutabelle benchmarks are run continuously on one lxlabbroy machine in pretty much the same way. The most important weakness at the moment is the lack of good plotting facilities for this sort of data. A student (Michael Kerscher) is currently working on that, with promising first results. Limitations === - Missing email notification Here is some room for discussion: What would be a good notification scheme? Since tests are now run continuously, sending an email after each run is not really an option. Should we simply go for a daily summary? More sophisticated options are possible (e.g., notify the author of a broken changeset when all its parents are working), but these require some thought. - Scheduling strategies could be better sometimes - Plotting (see above) - ... Alex ___ 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] [isabelle] Congruence rules for the code preprocessor
Hi Andreas,
the following ML line should do the job of adding the congruence rule in
your case:
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm conj_cong}]) *}
Before we add yet another feature to the code generation setup in Isar,
we would like to understand your scenario.
Does it occur naturally when setting up the code generator or is it a
very special corner case in your specifications?
Lukas
On 05/29/2011 04:44 PM, Tobias Nipkow wrote:
Does the current attribute mechanism support selective attributes such
as [code_inline cong], maybe along the lines of [simp del]? If it
does, I assume it would be easy to add that information in the place
that Florian pointed to?
Tobias
Am 28/05/2011 14:45, schrieb Florian Haftmann:
Hi Andreas,
the code generator tutorial mentions that the simpset for the code
preprocessor can apply the full generality of the Isabelle simplifier.
But how can I add anything else other than unfold theorems? The
attributes code_unfold and code_inline do not accept declarations like
declare conj_cong[code_inline cong]
Is there a way in Isar to declare congruence rules to the preprocessor?
no, this can only be done on the ML level, cf.
http://isabelle.in.tum.de/reports/Isabelle/file/0f9534b7ea75/src/Tools/Code/code_preproc.ML#l10.
Maybe it would be worth thinking about transfering all simpset
declaration attributes also to code_inline.
Hope this helps,
Florian
___
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] New Testing Infrastructure -- status report
Hi Alex, In the past weeks, there has been some progress with our new testing infrastructure, which I would like to summarize here. Please give feedback, ask questions, and discuss. Great!! Thanks for the update. I just have one question related to testboard: Then, local changes can be pushed to testboard via hg push -f testboard I use queues a lot and usually do all testing before I qfinish the queued patches. Is there a Mercurial trick to push all the applied queues without qfinishing them first? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New Testing Infrastructure -- status report
hg push -f testboard I use queues a lot and usually do all testing before I qfinish the queued patches. Is there a Mercurial trick to push all the applied queues without qfinishing them first? hg push -f actually does push applied mq patches as normal changesets, so it should do exactly what you want. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Latex issue (Fwd: isabelle dist build failed)
My impression from fooling around a little is that this is a bug that has been
around for a year and a half. The comment seems to suggest that | no longer
works as an index item (even when protected using), so we have to give up
index entries for the symbols | and |-|. I wonder whether there is some sort of
workaround?
http://r.789695.n4.nabble.com/Recent-TeX-changes-and-R-package-manuals-td956056.html
(ii) there have been intermittent problems with (LaTeX) special
characters in indices. But (hyperref 6.79d)
Full support of makeindex’s encap feature (e.g.
\index{alpha|textbf}). \hyperpage and the formatting command are
cascaded via \hyperindexformat. Internally \index{alpha|textbf} is
transferred to \index{alpha|hyperindexformat{\textbf}}.
\hyperindexformat calls the formatting command in its first argument
with the page range as argument that is put into \hyperpage. The
formatting command may call \hyperpage itself, it will be disabled
automatically to prevent nested \hyperpage commands.
has broken '|' as an index item ('||' was already broken) so I added
some special-casing (this does look like a bug in hyperref).
Larry
On 30 May 2011, at 09:39, Alexander Krauss wrote:
Hi all,
The nightly isatest stopped working after the tex distribution on our servers
was updated to Tex Live 2010 (at least we suspect that this is the cause of
the problem).
This seems to be an obscure latex problem that arises when buliding
doc-src/Logics. It seems that the (generated!) file logics.ind is somehow
malformed, which makes the subsequent tex run crash.
Could someone who knows more about this document setup look into this issue?
Steps to reproduce:
* Log into macbroy20-28
* On some repository clone, go to ~~/doc-src/Logics and run
make clean dvi
Note that the regular nightly isatest will not run until this is fixed,
because it first builds the documentation (as part of the distribution). The
new testing framework is not affected by it (since it effectively ignores
documentation at the moment).
Alex
Original Message
Subject: isabelle dist build failed
Date: Mon, 30 May 2011 00:18:04 +0200
From: isat...@macbroy28.informatik.tu-muenchen.de (Account Isatest)
To: kra...@in.tum.de
Could not build isabelle distribution. Log file available at
macbroy28:/home/isatest/log/isatest-makedist-2011-05-30.log
___
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] Latex issue (Fwd: isabelle dist build failed)
It seems it can be fixed by
(a) using ! rather than | as the sort key (the sorting of special symbols is
arbitrary anyway)
(b) using \char124 to denote the | symbol
I would expect to see this problem in any index entry involving the | symbol.
Larry
On 30 May 2011, at 14:58, Lawrence Paulson wrote:
My impression from fooling around a little is that this is a bug that has
been around for a year and a half. The comment seems to suggest that | no
longer works as an index item (even when protected using), so we have to
give up index entries for the symbols | and |-|. I wonder whether there is
some sort of workaround?
http://r.789695.n4.nabble.com/Recent-TeX-changes-and-R-package-manuals-td956056.html
(ii) there have been intermittent problems with (LaTeX) special
characters in indices. But (hyperref 6.79d)
Full support of makeindex’s encap feature (e.g.
\index{alpha|textbf}). \hyperpage and the formatting command are
cascaded via \hyperindexformat. Internally \index{alpha|textbf} is
transferred to \index{alpha|hyperindexformat{\textbf}}.
\hyperindexformat calls the formatting command in its first argument
with the page range as argument that is put into \hyperpage. The
formatting command may call \hyperpage itself, it will be disabled
automatically to prevent nested \hyperpage commands.
has broken '|' as an index item ('||' was already broken) so I added
some special-casing (this does look like a bug in hyperref).
Larry
On 30 May 2011, at 09:39, Alexander Krauss wrote:
Hi all,
The nightly isatest stopped working after the tex distribution on our
servers was updated to Tex Live 2010 (at least we suspect that this is the
cause of the problem).
This seems to be an obscure latex problem that arises when buliding
doc-src/Logics. It seems that the (generated!) file logics.ind is somehow
malformed, which makes the subsequent tex run crash.
Could someone who knows more about this document setup look into this issue?
Steps to reproduce:
* Log into macbroy20-28
* On some repository clone, go to ~~/doc-src/Logics and run
make clean dvi
Note that the regular nightly isatest will not run until this is fixed,
because it first builds the documentation (as part of the distribution). The
new testing framework is not affected by it (since it effectively ignores
documentation at the moment).
Alex
Original Message
Subject: isabelle dist build failed
Date: Mon, 30 May 2011 00:18:04 +0200
From: isat...@macbroy28.informatik.tu-muenchen.de (Account Isatest)
To: kra...@in.tum.de
Could not build isabelle distribution. Log file available at
macbroy28:/home/isatest/log/isatest-makedist-2011-05-30.log
___
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] Latex issue (Fwd: isabelle dist build failed)
There were broken index entries in most of the old documentation. For some
reason, the | symbol didn't cause a problem in the tutorial. One index entry
here was fixed to use ?? (as opposed to !) as the sort key.
Larry
On 30 May 2011, at 15:28, Lawrence Paulson wrote:
It seems it can be fixed by
(a) using ! rather than | as the sort key (the sorting of special symbols is
arbitrary anyway)
(b) using \char124 to denote the | symbol
I would expect to see this problem in any index entry involving the | symbol.
Larry
On 30 May 2011, at 14:58, Lawrence Paulson wrote:
My impression from fooling around a little is that this is a bug that has
been around for a year and a half. The comment seems to suggest that | no
longer works as an index item (even when protected using), so we have to
give up index entries for the symbols | and |-|. I wonder whether there is
some sort of workaround?
http://r.789695.n4.nabble.com/Recent-TeX-changes-and-R-package-manuals-td956056.html
(ii) there have been intermittent problems with (LaTeX) special
characters in indices. But (hyperref 6.79d)
Full support of makeindex’s encap feature (e.g.
\index{alpha|textbf}). \hyperpage and the formatting command are
cascaded via \hyperindexformat. Internally \index{alpha|textbf} is
transferred to \index{alpha|hyperindexformat{\textbf}}.
\hyperindexformat calls the formatting command in its first argument
with the page range as argument that is put into \hyperpage. The
formatting command may call \hyperpage itself, it will be disabled
automatically to prevent nested \hyperpage commands.
has broken '|' as an index item ('||' was already broken) so I added
some special-casing (this does look like a bug in hyperref).
Larry
On 30 May 2011, at 09:39, Alexander Krauss wrote:
Hi all,
The nightly isatest stopped working after the tex distribution on our
servers was updated to Tex Live 2010 (at least we suspect that this is the
cause of the problem).
This seems to be an obscure latex problem that arises when buliding
doc-src/Logics. It seems that the (generated!) file logics.ind is somehow
malformed, which makes the subsequent tex run crash.
Could someone who knows more about this document setup look into this issue?
Steps to reproduce:
* Log into macbroy20-28
* On some repository clone, go to ~~/doc-src/Logics and run
make clean dvi
Note that the regular nightly isatest will not run until this is fixed,
because it first builds the documentation (as part of the distribution).
The new testing framework is not affected by it (since it effectively
ignores documentation at the moment).
Alex
Original Message
Subject: isabelle dist build failed
Date: Mon, 30 May 2011 00:18:04 +0200
From: isat...@macbroy28.informatik.tu-muenchen.de (Account Isatest)
To: kra...@in.tum.de
Could not build isabelle distribution. Log file available at
macbroy28:/home/isatest/log/isatest-makedist-2011-05-30.log
___
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] [isabelle] Congruence rules for the code preprocessor
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where test xs = (last xs = 0)
definition test2 where test2 xs = (xs ~= [] test (rev xs))
(* Optimized implementation for test with context condition *)
lemma test_rev: xs ~= [] == test (rev xs) = (hd xs = 0)
unfolding test_def by(simp add: last_rev)
declare conj_cong[cong] test_rev[simp]
thm test2_def test2_def[simplified]
lemma test2 xs = (xs ~= [] test (rev xs))
apply simp
oops
The [simplified] attribute does apply the test_rev equation, but the
simp method in the proof does. Apparently, the same issue prevents the
code preprocessor from optimizing the code for test:
The simplifier behaves differently when working with free variables or
schematic variables.
Tobias can probably give a more precise answer how it behaves
differently (and why).
I will change the code preprocessor, so that you get the intended behaviour.
It might be worth discussing if the simplified attribute should be
changed to do the same thing.
Lukas
lemmas [code_inline] = test_rev test_rev[folded List.null_def]
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm
conj_cong}]) *}
code_thms test2
test2 is still implemented in terms of test (rev xs)
How can I unfold test_rev in test2_def?
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
