* More flexible generation of measure functions for termination proofs:
Measure functions can be declared by proving a rule of the form
is_measure f and giving it the [measure_function] attribute. The
is_measure predicate is logically meaningless (always true), and
just guides the heuristic. To
Hi Chris,
I just retrieved Isabelle from source control (Mercurial) and am
compiling with PolyML 5.2 under cygwin. I get a segfault from polly
compiling Pure.
That's weird.
Should I try bisecting this, and if so, what revision
should I start at? I haven't previously compiled Isabelle.
Brian Huffman wrote:
I, for one, am rather alarmed at the hurdles that Amine was forced to
overcome to do a simple merge of two theories.
I agree.
I think that the automatic class-instantiations should be disabled
immediately, and replaced with a new top-level command so that these
Lawrence Paulson wrote:
I have just done a fetch and can no longer build Isabelle/HOL.
confirmed for current tip: 0059238fe4bc
Alex
Has anyone else noticed that axiom True_or_False implies axiom
iff? (You can just do a proof by cases on P and Q.)
Here the case seems a little different, as eq_reflection is probably not
involved (or is it?). So maybe this is really redundant, but I am not sure.
I'm guessing that the
Brian Huffman wrote:
On Thu, Nov 12, 2009 at 4:52 AM, Makarius makarius at sketis.net wrote:
Anyway, can you still derive iff from a more conventional classical rule
without equality?
I just had a go at this, and I don't think it's possible.
Using the classical axiom P | ~ P, the proof
Hi Dominique,
Just to make sure I understand this correctly: The proof term that is
stored with a theorem will contain no nonempty sorts at all (not even
in intermediate proof steps)?
Yes. Unfinished proofs can still contain them, but they are normalized
away when the theorem is
Makarius wrote:
On Wed, 13 Jan 2010, Jasmin Blanchette wrote:
2. Generalize atp_manager.ML so that it can manage arbitrary
assistants, which are tools that take a goal and produce a message
-- not just ATPs -- and rename it HOL/Tools/assistant.ML.
Makarius wrote:
Although the ATP manager
Hi Brian,
added 605 changesets with 1325 changes to 175 files
Wow! What just happened?
Makarius merged in a long line of development concerning the interface
from a previously separate repository: c13e168a8ae6 through e596a0b71f3c.
Alex
Dear all,
Our web servers got upgraded, which broke the web frontend of the
Isabelle repository (and others). I managed to restore the basic
functionality (pull, browse), but without the customized style sheets.
Pushing over ssh was not affected anyway.
If you observe any unexpected behaviour
Hi Simon,
(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic tac rl =
let
val ctxt = Variable.thm_context rl;
val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
in
(case Seq.pull (tac st) of
NONE = raise THM (rule_by_tactic, 0, [rl])
|
Hi Brian,
Here are my thoughts:
- The termination prover uses the global simpset (clasimpset actually),
since I explicitly want it to pick up lemmas from the user. In practice,
I have never seen a termination proof break because of a bad simp rule
declared by the user. However, there is alse
Hi Brian,
Finally, the unfolding rule is used to prove the original equations.
This part uses the user-supplied fixrec_simp rules. The unfolding rule
is substituted on the LHS, and then the resulting goal is solved using
the simplifier.
(4) mapL$f$LNil = LNil
(5) x ~= UU == mapL$f$(LCons$x$xs)
Is there a better name for Rat.normalize?
IMHO, in most contexts, Rat.normalize is a more descriptive name than
normalize. If I had to invent a base name, it would probably be
normalize_rat or rat_normalize... So I would suggest hide (open).
Alex
Makarius wrote:
* There is a minimal test on x86-linux for
http://isabelle.in.tum.de/repos/isabelle with results being published
on testboard. (Maybe Alex can explain how to access them.)
The results can be accessed at
https://www4.in.tum.de/~krauss/hg/testboard/
The last run did
Hi Lars,
You are mis-reading the schematic goal below:
lemma
ALL (x::nat). x = y == False
apply (erule allE)
After this step, the subgoal ?x = y == False remains, which cannot be
proven. Else, we could prove:
schematic_lemma foo: ?x = y == False
sorry
lemma False by (auto intro: foo[of
Hi Thomas,
Thanks for digging into this. The concrete patch is exactly what was
needed to advance this discussion. Here are a few comments. I am sure
others will have more...
I attach the resulting patch. After
several rounds of bugfixes and compatibility improvements, it requires
23 lines
Hi Thomas,
Thomas Sewell wrote:
I should clear up some confusion that may have been caused by my
mail. I was trying to avoid repeating all that had been said on this
issue, and it seems I left out some that hadn't been said as well.
This approach avoids ever deleting an equality on a Free
Andreas Schropp wrote:
On 08/24/2010 06:35 PM, Makarius wrote:
Just like global types/consts/defs, local fixes/assumes merely
generate an infinite collection of consequences. The latter is what
you are working with conceptually, but it is not practical. So the
system provides further slots
Hi Thomas,
Thomas Sewell wrote:
It's interesting that my innocent thread on hypothesis substitution
has been hijacked into a discussion about context-aware coding
guidelines.
There is still hope if we move the unrelated discussions to another
thread...
I have another small comment on the
Florian Haftmann wrote:
What I have to address is that
you cannot be sure that a given name is already used, regardless how
many prefices you add.
There is a bit more to this story:
Ideally, the internals of a package should be completely invisible
unless a user explicitly chooses to look at
* New command 'partial_function' provides basic support for recursive
function definitons over complete partial orders. Concrete instances
are provided for i) the option type, ii) tail recursion on arbitrary
types, and iii) the heap monad of Imperative_HOL. See
HOL/ex/Fundefs.thy and
Makarius wrote:
I would say it is virtually impossible to experiment with new commands
in Proof General. One needs to produce isabelle-keywords.el in batch
mode first, and then continue interactively.
My standard workaround is to edit isar-keywords.el manually, ignoring
the WARNING IN
Makarius wrote:
Grepping through the sources for alt_name right now, I get the
impression that there was a second motivation: make really sure that the
synthesized big_rec_name variations really work in the target
context. Due to loss of information in base_name, it could in principle
clash
Dear list, (and Makarius in particular :-) )
I remember some offline discussions last year about having an Isabelle
tool that extracts file dependencies from theory sources (probably
starting from some special session file, which specifies the root
theories) and outputs it in a simple textual
Dear all,
This mailing list is becoming an important resource for
development-related questions and discussions. To reflect this and make
older discussions more accessible, the list archives are now mirrored at
two public sites, which allow more convenient searching and browsing via
a web
Makarius wrote:
Here are some examples for the isabelle scala toplevel:
[...]
Thanks, these are good pointers.
Unfortunately, this is (once again) harder than I thought. Here are the
issues/questions:
- Relative paths are not resolved by the current simple parser. I
remember that there used
Hi Michael,
Thanks, Alex. Indeed, the effect I'm after is like using setup {* *},
but ultimately I'd like this effect to be produced by calling a tactic,
i.e. let a tactic make updates to the current theory when invoked using
'apply (tac...)'.
AFAIK, this is impossible. Tactics/methods
Hi Lucas,
Nice failure :-)
datatype Ta = C_2 nat nat | C_1 Ta nat
fun f where
f (C_2 a b) c = c
| f (C_1 a b) c = f a (f a (f a (f (C_1 a b) b)))
(* ... after a long time...
constants
f :: Ta ⇒ nat ⇒ nat
Exception.
At command fun.
*)
This is the termination prover looping. It keeps
Dear all,
I want to report on the current state of smlnj testing.
Currently, the nightly isatest only covers the HOL image and
HOL-Library. More wasn't really feasible in a nightly-build setting on
a machine that is used interactively during the day.
Now we have a dedicated machine
Clemens Ballarin wrote:
JinjaThreads doesn't seem to run out of the box (on macbroy2, with
Poly/ML 5.3.0). It seems to run out of memory.
I use ML_OPTIONS=-H 500, but I would assume the AFP sets this
appropriately.
Probably this is a known issue, but I don't know where to check for the
Hi all,
(must add my 2ct, too)
Concerning the content of the next release:
Brian wrote:
What exactly makes it major? Judging by the NEWS file, it looks
like 2009-2 introduced about as many new features as the upcoming
release will. Is there any new feature in particular that is
considered a
The question is if PG 4.1 converges sufficiently fast for Isabelle2011,
and if we should switch to the PGIP update for floating point settings.
This would mean to discontinue 4.0 and 3.x altogether.
I've been using PG 4.1 for a while now from cvs, and it works nicely,
except that I've
* 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.
(please keep postings to isabelle-dev in English)
Tobias Nipkow wrote:
Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese
Fehlermeldung:
More precisely, the error occurs (almost) daily since January 11th,
according to my email archive.
Fuehlt sich hier jemand zustaendig?
So
Lawrence Paulson wrote:
Does anybody know what to do here?
Larry
~/isabelle/Repos: hg push
pushing to http://isabelle.in.tum.de/repos/isabelle
searching for changes
http authorization required
realm: Mercurial repositories
user:
Nothing is failing. It is just that pushing over http is
Dear all,
Unfortunately, Mirabelle is broken since aa8dce9ab8a9 ('discontinued
legacy load path;'). It relied on the implicit path, since it generates
a modified version of a theory file somewhere in /tmp, and then
processes that file using 'use_thy' in a raw isabelle_process. The
imports of
So I am wondering if the system could provide a variant of use_thy(s),
which takes an explicit master path and basically interprets the given
theory as if it would reside in that path. Probably, similar
functionality is already available for PG interaction. Of course any
other solution would
On 03/22/2011 10:17 PM, Makarius wrote:
It seems to have recovered, e.g. in 626fcf4a803e. Are you now the
Mirabelle maintainer?
I wouldn't go that far, as I know nothing about most Mirabelle
internals. I just needed to use it, so I fixed it with Sascha's help.
This is part of another attempt
Can anybody say where AFP is tested and if there are statistics accumulating?
The AFP test is currently still running in Sydney and accumulating the usual
data.
I've copied the logs over to ~/afp/log on macbroy*
There are also some runs being performed at TUM, but they are unofficial
and
Hi Brian,
I just noticed this error message from primrec if you write a
specification that is not primitive recursive. Here is a simplified
example:
primrec foo :: nat = nat where
foo 0 = 1 | foo (Suc n) = foo 0
*** Extra variables on rhs: foo
*** The error(s) above occurred in definition
What is the status of primrec anyway, in the light of fun(ction)?
It is still used
(a) for didactical reasons, to teach primitive recursion over datatypes,
(b) for bootstrapping purposes within HOL-Plain,
(c) since it is faster than fun, as it merely instantiates a combinator, and
(d) for
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
Hi all,
Now that this topic is already active, here is more:
In a small course here at TUM
(http://www4.in.tum.de/lehre/vorlesungen/perlen/SS11/) we are also using
jedit exclusively for the first time, and I can confirm the observation
that it makes it slightly easier for newbies to get
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
On 07/12/2011 01:18 PM, Makarius wrote:
On Tue, 12 Jul 2011, Alexander Krauss wrote:
sed -i 's/THE_VERSION/$(hg id)/g' version.ML
isabelle usedir ...
Actually, a similar thing happens when an isabelle distribution is
built from a repository clone.
Alex needs to do this because he his
On 07/12/2011 11:15 PM, Florian Haftmann wrote:
Hi Cezary (et al),
first, thanks a lot for your efforts, this is a valuable contribution!
There are a number of obvious things that could
be done with it, like you mention Isabelle settings but also proper
use of
local theories (this would avoid
[...]
Can you tell me how
I should do in the proof of the lemma continues to Isabelle runs through
here?
It was already pointed out that such questions are off-topic for this
list. Please repost to isabelle-us...@cl.cam.ac.uk !
Alex
___
Hi all,
with Cezary's guidance, I set up mira configurations for building the
proofs bundle from the HOL Light repository and for running the
HOL-Generate-HOLLight with that bundle, cf.
http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3
for the first
Hi Matthieu,
I have written a little ML library allowing to automatically prove, in most
cases, instantiations of types (typedefs, records and datatypes) as countable
(see ~~/src/HOL/Library/Countable).
It seems that for datatypes we now have such functionality, implemented
four weeks ago by
On 07/21/2011 09:47 PM, Gerwin Klein wrote:
The idea has potential for generalisation. Could we turn this into
something similar to Haskell's deriving?
The command would take a datatype and a list of instantiation methods
that each know how to instantiate a datatype for a specific type
class,
On 07/21/2011 04:25 PM, Steven Obua wrote:
Actually, there is a third code generator hidden somewhere in
Isabelle.
If you are talking about what I know under the name Compute Oracle,
then rest assured that it is hidden well enough that the chance of some
user accidentially confusing it with
datatype foo =
deriving countable, finite,
Tobias also mentioned set_of, map_of, etc. But since these aren't
class instantiations (we have no constructor classes such as functor),
we end up with the good old generic datatype interpretation (roughly:
datatype - theory - theory).
So it
Anyway, the standard procedure for removal of old stuff is to start
marking it as old or legacy in the NEWS, and emitting suitable
legacy_warnings.
I will follow that standard procedure, once all occurrences of the old
code generator invocations are replaced.
Put in legacy warnings already
On 08/03/2011 12:34 PM, Lawrence Paulson wrote:
Many thanks for your analysis. It looks like an interaction involving fix and
bound variables.
Not too fast :-)
We must now peel off the various layers of Isar (recall that show is
just a normal refinement step), to get closer to the problem.
Hi all,
The mira framework, which serves our continuous builds, is currently
down, since I messed something up while updating the data representation
in the database. You can still browse the reports as usual, but no new
tests are being run at the moment.
I hope that I can get this fixed
On 08/07/2011 02:53 PM, Alexander Krauss wrote:
The mira framework, which serves our continuous builds, is currently
down, since I messed something up while updating the data representation
in the database.
We're back to normal operation.
Alex
Florian: Is your modified Isabelle repo available for cloning, so we
can play with it? If so, I might be able to find an answer to my own
question...
You can clone directly from the http:// location:
hg clone http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set
or, faster, clone
On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
The benefits of getting rid of set were smaller than expected but quite
a bit of pain was and is inflicted.
Do you know of any more pain, apart from what Florian already mentioned?
Sticking with something merely to
avoid change is not a strong
On 08/12/2011 01:01 PM, Lawrence Paulson wrote:
(I'm trying to imagine
some sort of magic operator to ease the transition between sets with
various forms of tupling and relations.)
These tools exist to some extent, as the attributes [to_set] and
[to_pred]. It is used a few times in the
On 08/12/2011 02:16 PM, Tobias Nipkow wrote:
Surely we want to maintain both inductive and inductive_set?
This is what Florian's experiment does. It basically reverts the 2008
transition, but not the 2007 one.
Alex
___
isabelle-dev mailing list
I couldn't update ~isatest/hg-isabelle manually, because some files
in ~isatest/hg-isabelle/.hg/store belong to user krauss and isatest
doesn't seem to have enough permissions. Alex, could you please fix
these?
Oops... Restored permissions and updated.
Alex
On 08/18/2011 02:16 PM, Florian Haftmann wrote:
* (maybe)
hide_fact (open) Set.mem_def Set.Collect_def
to indicate that something is going on with these
maybe also declare them [no_atp], to avoid sledgehammer-generated proofs
that we know are going to break one release later...?
Hi all,
Here are some critical questions/comments towards two of Florian's
initial arguments pro 'a set.
[...]
* Similarly, there is a vast proof search space for automated tools
which is not worth exploring since it leads to the »wrong world«, making
vain proof attempts lasting longer
On 08/19/2011 01:31 AM, Gerwin Klein wrote:
On 19/08/2011, at 5:56 AM, Alexander Krauss wrote:
* Similarly, there is a vast proof search space for automated
tools which is not worth exploring since it leads to the »wrong
world«, making vain proof attempts lasting longer instead just
failing
On 08/20/2011 01:18 AM, Florian Haftmann wrote:
A typical example for what I was alluding to can be found at:
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/6e3e9c6c5062#l1.37
Observe the following proof:
lemma part_equivpI: (\existsx. R x x) \Longrightarrow symp R
Hi,
This took me a bit longer to answer properly, but anyway:
On 07/24/2011 05:05 PM, Makarius wrote:
The old recdef package is another ancient duplicate that is mostly used
in old manuals now. Is there a scheme for eventual removal?
The situation is a bit subtle.
Unfortunately, the
On 08/24/2011 03:36 PM, Lawrence Paulson wrote:
I've just been trying to get the proofs working, not to simplify them
or even to understand them. Incidentally, let there be no illusions
about people accidentally stumbling into a mixture of sets and
predicates. Some of these theories were clearly
The global axiom is
EX x. x : A == type_definition Rep Abs A
allowing local typedefs whenever non-emptiness of A is
derivable, even using assumptions in the context.
This is an interesting discussion, but totally off-topic in this thread
(whose main content is already growing very large.)
Florian Haftmann wrote:
envisaged working plan
--
a) general
* continue discussion about having set or not, end with a summary (for
the mailing list archive)
Among all the technical details about the HOW, the WHY part of this
discussion seems to have come to a halt. Here
Here's an example. After unfolding null_def, the user invoked Sledgehammer and asked
for an Isar proof. The proof - ... qed block after that is generated by Sledgehammer:
lemma null xs == tl xs = xs
proof -
assume nx: null xs
show tl xs = xs
using `null xs`
partial_function(option) foo :: nat list \Rightarrow unit option
where foo x = foo x
works, but
partial_function(option) foo :: 'a list \Rightarrow unit option
where foo x = foo x
yields the following error message.
*** exception THM 0 raised (line 1175 of thm.ML): instantiate: type
Alex
Hi Lukas,
I reset the testboard repository to start with a clean clone from the
development repository and now everything should work again.
If anyone is eager to restore the old testboard's changesets, we are
happy for any assistance, otherwise we will discard them within the next
week, if no
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 09/26/2011 11:38 PM, Makarius wrote:
isatest will also test http://isabelle.in.tum.de/repos/isabelle-release
within the next few weeks. (In the past I used to have a minimal isatest
for http://isabelle.in.tum.de/repos/isabelle but that was superseded by
On 10/16/2011 02:53 PM, Florian Haftmann wrote:
On lxbroy10, something is utterly wrong:
http://isabelle.in.tum.de/testboard/Isabelle/report/89d77033f6eb4dc196c199893871ae6d
Is anyone taking care for this?
Just tried to fix with Isabelle/efc2e2d80218.
In general, Lukas and Lars now also
Hi all,
Many of us have already seen isatest and other failures with of the
following form:
/tmp/mira/workbench/26748-140130062513920/Isabelle/lib/scripts/run-polyml:
line 77: 13588 Killed $POLY -q $ML_OPTIONS
...
make: ***
Lars Noschinski nosch...@in.tum.de wrote:
On 19.10.2011 23:36, Jasmin Christian Blanchette wrote:
Am 19.10.2011 um 22:34 schrieb Alexander Krauss:
Does anybody know if there is a straightforward translation of the
error codes 134/137 into English?
Just Google Unix exit codes.
E.g. 134
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
Hi all,
Some people might still remember this good old web page from Clemens,
which tells us how to work with the CVS version of Isabelle:
http://www4.in.tum.de/~ballarin/isabelle/repository.html
I now made an attempt to produce a modernized version of this, in order
to simplify the start
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
On 01/04/2012 10:30 PM, Makarius wrote:
Is there any reference to these details on some documentation (README,
manual, …)? A grep for Kodkod over the sources did not look very
promising.
A good starting point is the semi-official Admin/contributed_components
file, which seems to be also used
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 01/05/2012 10:22 AM, Makarius wrote:
I think one could publish ~isabelle/contrib_devel via HTTP, although
it would require some clean up and tuning, say to expand symlinks.
Another question is how to export the actual directory structure,
without maintaining explicit index.html and tar.gz
On 01/13/2012 06:24 PM, Makarius wrote:
I haven't been aware of that. The configuration goes back to myself, in
private communication with Alex. I did not check it later. In
4a892432e8f1 it is now more conventional, also tested manually to some
extend.
4a892432e8f1 merely modifies the setup
On 01/12/2012 03:43 PM, Stefan Berghofer wrote:
Quoting Makarius makar...@sketis.net:
Just to illuminate the general situation a bit, can you point to
relevant parts of your thesis, also the one of Konrad Slind for the
old version? Stefan had mentioned that at some point as everybody
knows,
On 01/18/2012 03:34 PM, Ondřej Kunčar wrote:
It's a bit annoying if you want to do
debugging on the ML level and you have to inspect every term by
inspecting its ML representation (which is really tedious for larger
terms).
This is a common problem, and everybody has come up with private
On 03/28/2012 11:33 PM, Cezary Kaliszyk wrote:
We have been working on a modernized reimplementation of HOL/Import,
for HOL Light. We think we are at a point where it could be pushed to
the main Isabelle repository replacing the old one.
This has happened now, cf. 4c7548e7df86.
A component
our system administrators just told me that our Munich compute server
(lxbroy10) still has many spare cycles, which we could use for more
testing and other measurements.
At the moment, there are two processes: one checking isabelle_makeall on
the testboard, another checking AFP_fast on the
Hi all,
while backporting HOL/Library/Set_Algebras to use type classes again (a
remaining point of the 'a set transition), I noticed that there is now a
clone of that file in HOL/ex. The changelog says:
changeset: 41581:c34415351b6d
user:haftmann
date:Sat Jan 15 20:05:29
On 04/16/2012 11:52 AM, Makarius wrote:
@Lukas: Thanks for pointing me to mercurial queues which are really
a great tool. Using queues it should be easily possible (even as an
external) to avoid the long pilage of private changes and public
commits.
The queues became quite popular early for
A completely different question is whether we can open testboard to
externals. This might reduce some communication overhead we are seeing
at the moment (I'm currently testing..., I have pushed..., etc.)
Essentially, this is just a matter of setting up a proper push-via-https
repository
Since
On 04/17/2012 05:41 PM, Tobias Nipkow wrote:
This is what I would call unwieldy: instead of typing-- or- (and having
them converted to the appropriate symbols) you always type-, but then you
have to select from a menue. I don't see the progress.
Could not agree more. These arrows are very
Hi,
I just got the following internal error from spass while trying out the
monolithic Windows bundle from Makarius:
theory Scratch
imports Main
begin
lemma A ⟶ B ⟹ A ⟹ B
sledgehammer
Sledgehammering...
spass: Internal error:
exception Empty raised (line 458 of library.ML)
On 04/23/2012 05:22 PM, Makarius wrote:
Here is an update of the test website for warming up a bit more
http://www4.in.tum.de/~wenzelm/test/website/
From the monolithic Windows App (with Windows 7):
The font in the little symbol replacement popup seems to be wrong: When
I enter ==, I just
I may as well be a bit more explicit. About seven Cambridge MPhil students were
given an assignment that included converting the following ML code into HOL and
proving theorems about it.
[...]
OK. See now e7e647949c95, as a reaction to this tragic story.
Alex
On 06/16/2012 02:11 PM, Jasmin Christian Blanchette wrote:
a) Subdirectories for each platform
/home/isabelle/contrib/
x86-linux/
x86_64-linux/
x86-cygwin/
...
Then, the universal component packages must be copied, symlinked or
hardlinked.
b) Different packages for
On 06/27/2012 02:03 PM, Makarius wrote:
On Wed, 27 Jun 2012, Florian Haftmann wrote:
Not sure what the status of »/home/isabelle/public_components« is.
See also this thread on the same topic:
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02157.html
On Thu, 28 Jun 2012, Tjark Weber wrote:
Directories would be more amenable to version control than tarballs, if
that makes a difference.
These are build artifacts, not sources, so SCM a la Mercurial is a
conceptual mismatch: There is no real notion of change (just monotonic
addition of new
On 06/29/2012 12:27 AM, Jasmin Christian Blanchette wrote:
Since our component store grows monotonically,
The way I see it, obsolete components should be removed, so as to
minimize confusion.
No reason for confusion here, since Admin/components tells you what you
need (and I am assuming
1 - 100 of 125 matches
Mail list logo
