On 09/30/2013 02:41 PM, Makarius wrote:
On Mon, 30 Sep 2013, Manuel Eberl wrote:
On 30/09/13 11:49, Makarius wrote:
On Mon, 23 Sep 2013, Manuel Eberl wrote:
I sent my changes to Alexander Krauss last Wednesday so that he can
review them.
We are now getting very close to the fork-point
On 09/27/2013 11:49 AM, Lars Noschinski wrote:
It might be a good idea to implement a strategy which tests the existing
heads in reverse chronological order (commits pushed last get tested
first), but I am not sure whether this information is available in
Mercurial (we have the commit date, but
On 09/11/2013 05:04 PM, Makarius wrote:
On Tue, 20 Aug 2013, Christian Sternagel wrote:
any opinions on making the type of monadic bind more general (see the
attached patch)?
This thread seems to be still open.
I now pushed the rebased change as eeff8139b3d8.
Do monadic people have a
Hi Chris,
[...]
When defining a function f, whose result type is T, it might be
necessary to peek under the hood in order to show termination. When
doing this manually, we destroy the abstraction and always have to
reason about the raw-level and even worse, also all the existing
constants with
On 08/17/2013 04:05 PM, Makarius wrote:
in the past few weeks the coming release has been mentioned in passing
several times. So far the precise schedule is not clear, but just from
the distance to Isabelle2013 and the amount of material that is about to
be finished for Isabelle2013-1, it has
Hi Chris,
any opinions on making the type of monadic bind more general (see the
attached patch)?
Generalizing bind itself would rather be a topic for ICFP or POPL, and I
cannot comment on that :-) Concerning the constant that represents it
syntactically, I would say that if it does not
Hi Jasmin,
On 08/06/2013 01:59 AM, Jasmin Blanchette wrote:
- The package registers a datatype interpretation to generate
congruence rules the case combinator for each type.
I guess it would make sense to have the package do that, or is there
a specific reason why it is better to do it in a
Hi Jasmin,
On 07/30/2013 05:40 PM, Jasmin Christian Blanchette wrote:
A rough, optimistic time plan follows.
[...]
Wow, I'm looking forward to it!
Let me quickly review the dependencies of the function package on the
datatype package:
- The package registers a datatype interpretation to
On 07/10/2013 07:25 PM, Makarius wrote:
Even simpler would be to invent a name for some variant of \omega that
is not considered a letter, and use that with \^sup as before. That
would be analogous to \epsilon vs. \some.
Does the mapping from Isabelle symbols to Unicode code points have to
Hi Chris,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Nice!
For completeness find my current adhoc_overloading.ML attached
Apart from the
On 05/30/2013 03:51 PM, Makarius wrote:
BTW, I've seen really good sources
recently: ACL2. They have a *strict* 80 char limit, and really good
writing style of essays, not code documentation.
This sounds interesting. Can you point to some examples of such essays?
Alex
Hi David,
On 04/03/2013 09:18 AM, David Greenaway wrote:
On 02/04/13 21:17, Makarius wrote:
before you send more patches, can you please go back to the very start
of the mail thread from last time, which contains a lot of hints how
things are done, including pointers to the documentation.
I
On Sat, 9 Mar 2013, Lars Noschinski wrote:
This behaviour only popped up after working with one session for a
longer time and jEdit was having frequent hiccups then, so I guess
this was due to memory pressure (max memory usage was near the limit
of 1600m set for the JVM).
On 03/18/2013 01:29
On 03/18/2013 12:47 PM, Makarius wrote:
On Sat, 16 Mar 2013, Florian Haftmann wrote:
you have to watch the »Raw output« buffer (via Plugins - Isabelle).
Toplevel.debug and Runtime.debug are the same flag, with slightly
varying purpose over the years, but now it is just for exception_trace
Hi all,
What is the current (as of, say, d5c95b55f849) method for getting
exception traces? I am trying to debug a low-level exception such as
exception Match raised (line 287 of term.ML)
which happens somewhere below partial_function. Some years ago there
used to be Toplevel.debug flag,
hg push -f testboard
pushing to
ssh://nosch...@lxbroy10.informatik.tu-muenchen.de//home/isabelle-repository/repos/testboard
searching for changes
remote: abort: could not lock repository
/home/isabelle-repository/repos/testboard: Permission denied
abort: unexpected response: empty string
It
On 12/20/2012 06:22 PM, Makarius wrote:
I just had a long phone call with Franz Huber, the local system admin
person. All the macbroy20..29 and lxlabbroyX machines involved here
use the same OpenSuse 12.2 with that hg 2.4. So just empirically that
looks like the problem -- breakdowns started
On 12/20/2012 12:20 AM, Alexander Krauss wrote:
I am now writing this up for the hg mailing list, since we now may
have enough information to get help tracking it down...
I posted a question here:
http://www.selenic.com/pipermail/mercurial/2012-December/044783.html
and there are some answers
On 12/05/2012 10:50 PM, Gerwin Klein wrote:
I am unsure how to proceed debugging these hangs. I will try some
other machines and see if it is correlated with MacOS X or if it is
something else.
Since no log file gets produced and no information comes out of tty
mode, it's not even clear to me
Quoting Clemens Ballarin balla...@in.tum.de:
[...]
pushing to
ssh://balla...@macbroy2.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
searching for changes
remote: Not trusting file
/mnt/nfsbroy/home/isabelle-repository/repos/isabelle/.hg/hgrc from
untrusted user
Hi all,
Today, I've completed the (long overdue) migration of the mira database
from Florian's old machine to a proper server (hosted on
isabelle.in.tum.de).
Since the replication feature had some problems (probably due to the
version mismatch), I moved the data over by dumping to a file
Hi all,
It seems that the main Isabelle repository got corrupted again and is
currently unavailable.
Since the error seems to be the same as last time, I expect to be able
to fix it quickly. Apparently, the error is correlated with me pushing
some changes in, so I guess I'll have to try to
It seems that the main Isabelle repository got corrupted again and is
currently unavailable.
OK, it's back for now...
Alex
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On 08/06/2012 12:06 AM, Makarius wrote:
There is presently a problem with
http://isabelle.in.tum.de/repos/isabelle around rev ebbd70082e65 -- also
with local pushes or pulls, but it seems to work via ssh (at least for me).
The problem (a repository corruption for reasons we don't know yet) are
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
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
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 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
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
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
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
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
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
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
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
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 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/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/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/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
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
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
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
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
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: ***
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
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 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
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
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
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`
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
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.)
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
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/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
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/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
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/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
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/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
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/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.
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
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
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
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
[...]
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
___
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
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
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
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 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
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
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
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
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
(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
* 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 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
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
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
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
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
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
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
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
1 - 100 of 125 matches
Mail list logo
