* Command 'typ' supports an additional variant with explicit sort
constraint, to infer and check the most general type conforming to a
given given sort. Example (in HOL):
typ _ * _ * bool * unit :: finite
This refers to Isabelle/4aa5b965f70e.
Makarius
*** System ***
* The isabelle mkroot tool prepares session root directories for use
with isabelle build, similar to former isabelle mkdir for
isabelle usedir.
This refers to Isabelle/eeb4480b5877.
Makarius
___
isabelle-dev mailing list
Am 02.08.2012 um 23:20 schrieb Makarius:
BTW, there were other specialities in Collections, Refine_Monadic, and also
Huffman concerning document generation. These were rather unexciting, and
easily performed by regular system functions.
For Huffman, the fixdoc script is not critical. It
In Collections and refine-monadic, as far as I can remember, there are
two specialties:
1. We use a book document class rather than the default article, which
required some fine-tuning of the documents. We use text_raw
\chapter{...} instead of header .
2. We generate the userguide as a
On Fri, 3 Aug 2012, Jasmin Christian Blanchette wrote:
For Huffman, the fixdoc script is not critical. It replaces 'a with
\alpha and things like that. I can live without it. But what do you mean
by regular system functions?
This is how I first did it:
On Fri, 3 Aug 2012, Peter Lammich wrote:
In Collections and refine-monadic, as far as I can remember, there are
two specialties:
1. We use a book document class rather than the default article, which
required some fine-tuning of the documents. We use text_raw
\chapter{...} instead of header .
Is there really any *need* to have ruby produce theory sources? Browsing
through the outcome briefly, it looks very conventional: a few document
antiquotations and a few defininitions/theorems/interpretations issued in
Isabelle/ML should do the job. The bit of Isabelle/ML should be
On Thu, 2 Aug 2012, Gerwin Klein wrote:
The etc/sessions file should make that possible, although I'm not
opposed to Florian's proposal of fusing the two concepts into one file:
if ROOT supported a syntax construct that lists directories as in the
session file, we could have a thys/ROOT with
On Thu, 2 Aug 2012, Gerwin Klein wrote:
LighweightJava is a worrisome example, because it needs an external tool
to generate the sources which in the meantime have been updated manually
during maintenance, despite multiple rather prominent warnings of the
form:
Note:This file
On Thu, 2 Aug 2012, Makarius wrote:
On Thu, 2 Aug 2012, Gerwin Klein wrote:
LighweightJava is a worrisome example, because it needs an external
tool to generate the sources which in the meantime have been updated
manually during maintenance, despite multiple rather prominent warnings
of the
On Thu, 2 Aug 2012, Makarius wrote:
Note that generated theory sources are not supported by isabelle build
-- it simply does not fit into the concept; this is no longer shell +
make scripting.
So, what do we do with the entries that need them?
The other entry is thys/Collections. It
On 03/08/2012, at 7:02 AM, Makarius makar...@sketis.net wrote:
On Thu, 2 Aug 2012, Makarius wrote:
On Thu, 2 Aug 2012, Gerwin Klein wrote:
LighweightJava is a worrisome example, because it needs an external tool to
generate the sources which in the meantime have been updated manually
On Sat, 28 Jul 2012, Makarius wrote:
In particular, we need to devise a plan to upgrade:
* mira (?)
Is there any mira expert who is not on vacation? Otherwise I have to
start understanding its setup myself.
Makarius
___
isabelle-dev
On 08/01/2012 11:52 AM, Makarius wrote:
Is there any mira expert who is not on vacation? Otherwise I have to
start understanding its setup myself.
I am already looking into this.
Alex
___
isabelle-dev mailing list
isabelle-...@in.tum.de
This is an update on the build configuration for AFP:
Isabelle/4dd1d4585902
AFP/4892fed712e1
afp-build/a6ccf93b0574 (see https://bitbucket.org/makarius/afp-build)
The Scala and ML functions of afp-build guess the content of the original
ROOT.ML and IsaMakefiles, and turn them into
On Tue, 31 Jul 2012, Makarius wrote:
This is an update on the build configuration for AFP:
Isabelle/4dd1d4585902
AFP/4892fed712e1
afp-build/a6ccf93b0574 (see https://bitbucket.org/makarius/afp-build)
This should be Isabelle/6004f4575645. In Isabelle/4dd1d4585902 the
Read-Black Tree tree
On Sun, 29 Jul 2012, Makarius wrote:
Here is a one-liner for private use in $ISABELLE_HOME_USER/ROOT:
session HOL-Test! in ~~/src/HOL = Pure + theories Nat
This works because $ISABELLE_HOME_USER is also a component.
Oops, the non-identifier name HOL-Test above needs to be quoted,
On 30/07/2012, at 3:04 AM, Makarius wrote:
On Sun, 29 Jul 2012, Gerwin Klein wrote:
The documents and outline are one major outcome (some might say the whole
point) of the AFP sessions. So we still need to test them in the nightly run
and some sessions will require special setup, e.g.
*** System ***
* Advanced support for Isabelle sessions and build management, see
system manual for the chapter of that name, especially the isabelle
build tool and its examples. Eventual INCOMPATIBILITY, as isabelle
usedir / make / makeall are rendered obsolete.
Two things come to my
Am 29/07/2012 03:16, schrieb Gerwin Klein:
On 29/07/2012, at 5:06 AM, Makarius makar...@sketis.net wrote:
For AFP, I would like to see a scheme without hardwired document option
within the ROOTs. Instead it can be provided for particular invocations of
isabelle build -o document=pdf etc.
On Sun, 29 Jul 2012, Gerwin Klein wrote:
The documents and outline are one major outcome (some might say the
whole point) of the AFP sessions. So we still need to test them in the
nightly run and some sessions will require special setup, e.g. other
programs to run before the document is
On Sun, 29 Jul 2012, Florian Haftmann wrote:
* Now, there are the ROOT file(s) and etc/sessions. I wonder whether
this can be unified further, e.g. having just one sessions file in . or
etc/.
Right now etc/sessions is unused. I merely added it pro-actively to
support a speculative scheme
On Sun, Jul 29, 2012 at 7:11 PM, Makarius makar...@sketis.net wrote:
The question is if HOL-Plain and HOL-Main still have any purpose. Full HOL
now takes 2min on a reasonably fast machine with 4 cores.
Images like HOL-Plain or HOL-Main are often useful when I am doing
development on libraries
On Sun, 29 Jul 2012, Brian Huffman wrote:
On Sun, Jul 29, 2012 at 7:11 PM, Makarius makar...@sketis.net wrote:
The question is if HOL-Plain and HOL-Main still have any purpose. Full HOL
now takes 2min on a reasonably fast machine with 4 cores.
Images like HOL-Plain or HOL-Main are often
On Sun, 29 Jul 2012, Makarius wrote:
Of course, if we can make it easy enough to build custom images, then
there is no practical reason to have HOL-Plain or HOL-Main set up by
default in the distribution.
I did not think of this option yet. It might be actually simple to set
that up
*** System ***
* Discontinued special treatment of Proof General -- no longer guess
PROOFGENERAL_HOME based on accidental file-system layout. Minor
INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS
settings manually, or use a Proof General version that has been
bundled as
*** System ***
* Advanced support for Isabelle sessions and build management, see
system manual for the chapter of that name, especially the isabelle
build tool and its examples. Eventual INCOMPATIBILITY, as isabelle
usedir / make / makeall are rendered obsolete.
* Discontinued obsolete
On 29/07/2012, at 5:06 AM, Makarius makar...@sketis.net wrote:
For AFP, I would like to see a scheme without hardwired document option
within the ROOTs. Instead it can be provided for particular invocations of
isabelle build -o document=pdf etc. This and build -j MAX should give a
great
cf. http://isabelle.in.tum.de/reports/Isabelle/rev/ffa0618cc4d4:
* Library/Debug.thy and Library/Parallel.thy: debugging and parallel
execution for code generated towards Isabelle/ML.
Florian
--
PGP available:
The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the configuration option z3_with_extensions. Minor
INCOMPATIBILITY.
On 04.06.2012 09:28, Sascha Boehme wrote:
The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the configuration option
I look forward to seeing some documentation on these increasingly mysterious
constructs… :-)
Larry
On 16 Apr 2012, at 11:14, Brian Huffman wrote:
On Sun, Apr 15, 2012 at 2:54 PM, Makarius makar...@sketis.net wrote:
* Auxiliary contexts indicate block structure for specifications with
On Tue, 17 Apr 2012, Lawrence Paulson wrote:
I look forward to seeing some documentation on these increasingly
mysterious constructs… :-)
It is pretty close to the original concept of section that you've
introduced with Florian Kammüller in 1998/1999, so it is much more basic
than locales +
On Mon, 16 Apr 2012, Brian Huffman wrote:
Finally we have a mechanism similar to Section in Coq, a more
lightweight alternative to locales.
This is what Larry Paulson and Florian Kammüller actually started in
1998/1999 and eventually became the fully-featured locale + interpretation
system
On Mon, 16 Apr 2012, Brian Huffman wrote:
Another good use case is recursive functions with many parameters that
don't change in recursive calls. For example, here's a recursion
combinator for binary integers:
context
fixes z0 z1 :: 'a
fixes f0 f1 :: 'a = 'a
begin
function bin_rec :: int
* Auxiliary contexts indicate block structure for specifications with
additional parameters and assumptions. Such unnamed contexts may be
nested within other targets, like 'theory', 'locale', 'class',
'instantiation' etc. Results from the local context are generalized
accordingly and applied to
On Thu, Mar 29, 2012 at 7:50 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
As it is now, theory »Code_Nat« is
not announced that prominently, but this is not that critical.
We should at least put an announcement in NEWS about Code_Nat.
However, you have talked about
However, you have talked about making the binary representation for
nat the default in HOL-Main, i.e. merging Code_Nat into the Nat/Num
theories. Are you still interested in doing this?
Definitely, among other related things. But I'm not very optimistic
this can be done before the end of
On Wed, Mar 28, 2012 at 9:15 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Btw. for the moment you have not transferred by additional changes
concerning Efficient_Nat etc. What are your plans for these? To wait
until the transition proper has fortified a little? Or
Hi Brian,
You had replaced Efficient_Nat.thy with a similar theory file named
Code_Numeral_Nat.thy. I chose to rename this back to Efficient_Nat
before doing the big merge, because it meant touching about a dozen
fewer files, and avoiding breaking lots of AFP entries. I also
reverted the
Hi Brian,
Good work!
There are still a couple of loose ends to take care of, which are
currently marked with BROKEN in the sources:
* Nitpick_Examples/Integer_Nits.thy: A call to nitpick on a goal with
negative numerals doesn't work. I expect the problem originates in
On Sun, 25 Mar 2012, Brian Huffman wrote:
As of 2a1953f0d20d, Isabelle now has a new representation for binary
numerals
Execellent, this is a big step forward in this important reform. It seems
we now have the main parts in place, so that we can start consolidating
towards the release over
On 03/26/2012 02:10 PM, Makarius wrote:
On Sun, 25 Mar 2012, Brian Huffman wrote:
As of 2a1953f0d20d, Isabelle now has a new representation for binary
numerals
Execellent, this is a big step forward in this important reform. It
seems we now have the main parts in place, so that we can
On Mon, 26 Mar 2012, Lukas Bulwahn wrote:
This problem is reproducible on our testboard servers. At the moment,
all tests of changesets after 2a1953f0d20d have to be manually aborted
because of that reason. I hope you find a solution quickly, otherwise we
should deactivate the Proofs-Lambda
On Mon, Mar 26, 2012 at 7:23 PM, Makarius makar...@sketis.net wrote:
On Mon, 26 Mar 2012, Lukas Bulwahn wrote:
This problem is reproducible on our testboard servers. At the moment, all
tests of changesets after 2a1953f0d20d have to be manually aborted because
of that reason. I hope you find a
As of 2a1953f0d20d, Isabelle now has a new representation for binary numerals:
*** HOL ***
* The representation of numerals has changed. We now have a datatype
num representing strictly positive binary numerals, along with
functions numeral :: num = 'a and neg_numeral :: num = 'a to
represent
* Command 'definition' no longer exports the foundational raw_def
into the user context. Minor INCOMPATIBILITY, may use the regular
def result with attribute abs_def to imitate the old version.
* Attribute abs_def turns an equation of the form f x y == t into
f == %x y. t, which ensures that
Next attempt on NEWS on sets committed.
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
On 01/04/2012 10:19 PM, Makarius wrote:
The difference of a fully integrated release bundle and a development
snapshot is increasing more and more -- since the bundles are getting
so advanced. I would not like to see the clear distinction between
production quality releases and arbitrary
On Thu, 5 Jan 2012, Lawrence Paulson wrote:
I think your point is that somebody who spent a lot of effort making
their code work with a development snapshot could be wasting their time,
because the next release could be as different and require everything to
be converted again.
Yes, but
Hi Jasmin,
Congratulations on your heroic effort for reintroducing set!
heroism and foolhardiness are close together…
I'm glad to report that Nitpick, Refute, Sledgehammer, and SMT_Example have
now been ported to handle set properly, and that the commented out examples
are live again.
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared. INCOMPATIBILITY, rephrase sets S used as
predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`.
For typical proofs, it is often sufficent to prune any tinkering with
former theorems
I did quite a few of these conversions. Generally the changes were
straightforward, EXCEPT for theories that explicitly treated sets as
predicates. In the former case, the strategy is to rigorously confine yourself
to set primitives, but in the latter case, you may find yourself with a
On Wed, 4 Jan 2012, Lawrence Paulson wrote:
It seems to me that we owe users an announcement on the mailing list so
that they know that this is coming. They can then download a development
snapshot to see what it will look like.
Coping with the delicacies introducing further challanges
On Wed, 4 Jan 2012, Florian Haftmann wrote:
BTW Nitpick_Examples should have been failing all over the place. If
they haven't, this indicates that neither of your two setups (macbroy2
and local machine) have Kodkod enabled.
Is there any reference to these details on some documentation
On Wed, 4 Jan 2012, Makarius wrote:
On Wed, 4 Jan 2012, Lawrence Paulson wrote:
It seems to me that we owe users an announcement on the mailing list so
that they know that this is coming. They can then download a development
snapshot to see what it will look like.
Coping with the
On Wed, 28 Dec 2011, Jasmin Christian Blanchette wrote:
Am 27.12.2011 um 13:03 schrieb Florian Haftmann:
There is a failure in Nitpick_Examples which is neither reproducible on
macbroy2 nor my local machine:
http://isabelle.in.tum.de/reports/Isabelle/report/14fe4e1bd31f4a9fab112f57669a1de5
On Mon, 26 Dec 2011, Florian Haftmann wrote:
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared. INCOMPATIBILITY, rephrase sets S used as
predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`.
For typical proofs, it is often sufficent
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared.
Good news.
(https://isabelle.in.tum.de/isanotes/index.php/Having_'a_set_back%23Roaring_ahead).
Do not expect stability before this list has boilt down.
Not stability, but a working isatest
Hi Florian,
On 12/26/2011 05:33 PM, Florian Haftmann wrote:
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared.
Good news.
(https://isabelle.in.tum.de/isanotes/index.php/Having_'a_set_back%23Roaring_ahead).
Do not expect stability before this list
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared. INCOMPATIBILITY, rephrase sets S used as
predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`.
For typical proofs, it is often sufficent to prune any tinkering with
former theorems
Quickcheck returns variable assignments as counterexamples, which
allows to reveal the underspecification of functions under test.
For example, refuting hd xs = x, it presents the variable
assignment xs = [] and x = a1 as a counterexample, assuming that
any property is false
* Renamed inner syntax categories num to num_token and xnum to
xnum_token, in accordance to existing float_token. Minor
INCOMPATIBILITY. Note that in practice num_const etc. are mainly
used instead.
This refers to Isabelle/c7a13ce60161.
Makarius
On Sun, Nov 20, 2011 at 9:52 PM, Makarius makar...@sketis.net wrote:
* Commands 'lemmas' and 'theorems' allow local variables using 'for'
declaration, and results are standardized before being stored. Thus
old-style standard after instantiation or composition of facts
becomes obsolete. Minor
On Tue, 22 Nov 2011, Brian Huffman wrote:
On Sun, Nov 20, 2011 at 9:52 PM, Makarius makar...@sketis.net wrote:
* Commands 'lemmas' and 'theorems' allow local variables using 'for'
declaration, and results are standardized before being stored. Thus
old-style standard after instantiation or
* Sort constraints are now propagated in simultaneous statements, just
like type constraints. INCOMPATIBILITY in rare situations, where
distinct sorts used to be assigned accidentally. For example:
lemma P (x::'a::foo) and Q (y::'a::bar) -- now illegal
lemma P (x::'a) and Q (y::'a::bar)
Hi Johannes,
I tried to reduce the runtime requirement of HOL-Probability by removing
some of the sublocale instantiations. As a lot of time is spend in
locale interpretation inside proofs.
Is the same interpretation repeated over and over? In that case the
corresponding proposition can be
I think this is a good idea.
Larry
On 22 Sep 2011, at 03:08, Brian Huffman wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
Legacy.thy that would not be imported by default, and would be
cleared out
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
Legacy.thy that would not be imported by default, and would be
cleared out after each release. When upgrading Isabelle, users could
import Legacy.thy as needed
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
Legacy.thy that would not be imported by default, and would be
cleared out after each release. When upgrading Isabelle,
On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
Legacy.thy that would not be imported by default, and would be
cleared out
On Wed, 21 Sep 2011, Brian Huffman wrote:
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban urb...@in.tum.de wrote:
I was able to put together replacement theorems for a few of these lemmas:
Inf_singleton ~ Inf_insert [where A={}, unfolded Inf_empty inf_top_right]
Sup_singleton ~ Sup_insert
In Java, there is a deprecated flag for such issues. Isabelle could
then issue
a warning whenever using a deprecated lemma --- like the legacy-warnings
it already issues when using some deprecated features (recdef, etc.)
You are assuming that you could flag theorems, and all tools know what
On Tue, 20 Sep 2011, Makarius wrote:
In the meantime I have investigated this a little bit. It seems that
HOL-Probability requires quite some memory even in minimalistic batch mode --
approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further 600 MB
for the editor process and the
On Thu, Sep 22, 2011 at 6:10 AM, Makarius makar...@sketis.net wrote:
On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
On 09/22/2011 05:00 PM, Brian Huffman wrote:
I actually like Peter's idea of a deprecated flag better than my
Legacy.thy idea. We might implement it by adding a new deprecated
flag to each entry in the naming type implemented in
Pure/General/name_space.ML. Deprecated names would be treated
On Thu, 22 Sep 2011, Brian Huffman wrote:
Anyway, if we are decided that the legacy phase for renamed/generalized
theorems is not useful, then there is no point in preserving the legacy
theorems sections in the libraries, is there? We might as well go ahead
and start removing all of these
On 18.09.2011 17:05, Makarius wrote:
On Tue, 13 Sep 2011, Lars Noschinski wrote:
I was irritated when Isabelle/jEdit complained about missing theory
files, when the files where obviously there (and loaded). Later I
found out, that this error is also displayed if there are any errors
On Tue, 13 Sep 2011, Lars Noschinski wrote:
I was irritated when Isabelle/jEdit complained about missing theory
files, when the files where obviously there (and loaded). Later I found
out, that this error is also displayed if there are any errors
(transitively) in these theory files.
Did
On 09/12/2011 07:29 PM, Florian Haftmann wrote:
Hi Lukas,
the rename
AssocList ~ AList_Impl
should sound
AssocList ~ AList
Nota bene:
T.thy – theory as intended to be used by other theoreis
T_Impl.thy – implementation for abstract type
Since ALists are not abstract, there is
On 06.09.2011 21:58, Makarius wrote:
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
isabelle jedit on the command line.
. Management of multiple theory files directly from the editor
buffer store -- bypassing the file-system (no requirement to save
files for checking).
On 09/13/2011 11:38 AM, Lars Noschinski wrote:
- The command line help shows some option -l to use a different
logic image, but this does not seem to work.
-l works perfectly for us: for instance,
/usr/local/isabelle/bin/isabelle jedit -l Isac Test_Isac.thy
runs all tests
On 13.09.2011 12:01, Walther Neuper wrote:
On 09/13/2011 11:38 AM, Lars Noschinski wrote:
- The command line help shows some option -l to use a different
logic image, but this does not seem to work.
-l works perfectly for us: for instance,
/usr/local/isabelle/bin/isabelle jedit -l Isac
Hi Lukas,
the rename
AssocList ~ AList_Impl
should sound
AssocList ~ AList
Nota bene:
T.thy – theory as intended to be used by other theoreis
T_Impl.thy – implementation for abstract type
Since ALists are not abstract, there is no AList_Impl.thy, but cf.
RBT_Impl.thy.
The rename
My impression is that NEWS and CONTRIBUTORS for the coming release is
still somewhat incomplete.
NEWS is not just for bad news -- infamous INCOMPATIBILITY entries -- but
for any user-relevant changes. If things are not user-relevant then
what is the point of doing them in the first place?
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
isabelle jedit on the command line.
. Management of multiple theory files directly from the editor
buffer store -- bypassing the file-system (no requirement to save
files for checking).
. Markup of formal entities
On Tue, 6 Sep 2011, Makarius wrote:
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
isabelle jedit on the command line.
The required build component is still the same:
http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz
Makarius
*** ML ***
* The inner syntax of sort/type/term/prop supports inlined YXML
representations within quoted string tokens. By encoding logical
entities via Term_XML (in ML or Scala) concrete syntax can be
bypassed, which is particularly useful for producing bits of text
under external program
On 07/11/2011 05:45 PM, Makarius wrote:
*** ML ***
* The inner syntax of sort/type/term/prop supports inlined YXML
representations within quoted string tokens. By encoding logical
entities via Term_XML (in ML or Scala) concrete syntax can be
bypassed, which is particularly useful for producing
*** ML ***
* Isabelle_Process.is_active allows tools to check if the official
process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop
(better known as Proof General).
See Isabelle/6bc8a6dcb3e0
Makarius
___
isabelle-dev mailing
*** Document preparation ***
* Antiquotation @{rail} layouts railroad syntax diagrams, see also
isar-ref manual.
* doc-src build process is independent of external rail executable.
See Isabelle/936cd1c493b4
Makarius
___
isabelle-dev mailing
* Theory loader: source files are identified by content via SHA1
digests. Discontinued former path/modtime identification and optional
ISABELLE_FILE_IDENT plugin scripts.
See also http://isabelle.in.tum.de/repos/isabelle/rev/703ea96b13c6
Makarius
* New term style isub as ad-hoc conversion of variables x1, y23 into
subscripted form x\^isub1, y\^isub2\^isub3.
For use in document preparation, e.g.,
lemma foo: P x1 x2 proof
text {*
@{thm (isub) foo}
*}
produces output with subscripts. Converts names of Frees, Vars and Bounds.
The upcoming release (which I guess will be called Isabelle 2011-0
Dispensable Debate) will have the following notable extensions to
locale interpretation:
* Locale interpretation commands 'interpret' and 'sublocale' accept
lists of equations to map definitions in a locale to appropriate
* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
(and thus refers to something like $HOME/.isabelle/Isabelle),
while the default heap location within that directory lacks that extra
suffix. This isolates multiple Isabelle installations from each
other, avoiding problems
On Fri, 29 Oct 2010, Lukas Bulwahn wrote:
* Quickcheck now has a configurable time limit which is set to 30
seconds by default. This can be changed by adding [timeout = n] to the
quickcheck command. The time limit for auto quickcheck is still set
independently, by default to 5 seconds.
I am
Unless I have a lapse of memory, the timeout specifications for s/h and
Nitpick are also in seconds, possibly with an s appended. As a user I
am glad about that, because I do not think in ms and would not like to
write 3 instead of 30.
Tobias
Makarius schrieb:
On Fri, 29 Oct 2010, Lukas
On Fri, 29 Oct 2010, Tobias Nipkow wrote:
Unless I have a lapse of memory, the timeout specifications for s/h and
Nitpick are also in seconds, possibly with an s appended. As a user I
am glad about that, because I do not think in ms and would not like to
write 3 instead of 30.
I have
As I said, I was entirely unconfused that it is in seconds, and am glad
of it. HOWEVER: there is indeed a confusing difference between s/h and
Nitpick on the one hand and q/c on the other hand:
quickcheck[timeout=30]
sledgehammer[timeout=30s]
And also in their response to the wrong format:
SMT's timeout option is also measured in seconds, and this is the
case since its beginning. I found this a natural decision, and no one
has ever objected to it.
Sascha
Tobias Nipkow wrote:
Unless I have a lapse of memory, the timeout specifications for s/h and
Nitpick are also in seconds,
601 - 700 of 766 matches
Mail list logo
