Makarius wrote:
It is not so easy to get an exception trace here. Wrapping up
Simplifier.generic_simp_tac as shown in the included changeset produces
the following result:
Exception trace - TYPE (Loose bound variable: B.7, [], [Bound 7])
Sign.type_check(2)typ_of(2)
[...]
On 05/27/2013 07:54 PM, Makarius wrote:
Here is another example for Isabelle/Pure, without schematic variables with
different types. It may be be tried before/after my change 3b9c31867707 from
today:
[...]
ML {*
val read = Syntax.read_term (Proof_Context.set_mode
On 04/12/2013 02:18 PM, Makarius wrote:
Just for completeness, I am posting here a self-contained example to expose the
problem.
It looks like I need to discuss it further with Stefan Berghofer, because he
made some reforms there in 2005 that now seem to crash on us.
Hi Markus
Hi Markus,
On 01/07/2013 10:45 AM, Makarius wrote:
On Fri, 4 Jan 2013, Stefan Berghofer wrote:
I am currently getting an exception Thread Thread creation failed after some
time when compiling HOL with PolyML 5.5.0 on a machine with quite a few CPUs (I am using
Isabelle repository version
Hi David,
On 01/07/2013 12:31 PM, David Matthews wrote:
Is there a limit on the number of threads per process in Linux? I haven't been
able to find anything about it.
Neither have I.
You could certainly hit limits on memory for stacks with a large number of threads
particularly if the
Hi David,
On 01/07/2013 12:45 PM, David Matthews wrote:
What does Thread.Thread.numProcessors() report? That's the number that will be
used for the GC threads.
It reports 24.
I'm not inclined to put an arbitrary limit on the number of threads. There are
certain parts of the GC process
Florian Haftmann wrote:
* This is mainly a question to Stefan: there are some theorems commented
out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes. I
guess this is due to a higher-order situation, but I would be reassuring
if you can confirm that.
Hi Florian,
I have fixed
Florian Haftmann wrote:
* This is mainly a question to Stefan: there are some theorems commented
out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes. I
guess this is due to a higher-order situation, but I would be reassuring
if you can confirm that.
Hi Florian,
this looks
Quoting Lawrence Paulson l...@cam.ac.uk:
I got this message several times when converting theories. There is
a workaround, but nevertheless, I think this is a bug.
Hi Larry,
the reason for this problem is the removal of the rules pred_equals_eq and
pred_subset_eq from the rule database used
Quoting Makarius makar...@sketis.net:
On Thu, 1 Dec 2011, Jasmin Christian Blanchette wrote:
I just pulled and updated (hg pull -u) from the main repository
and got these strange warnings:
Fügte 118 Änderungssätze mit 572 Änderungen zu 411 Dateien hinzu
warning: detected divergent renames
Alexander Krauss wrote:
In particular, Stefan discovered that replacing inductive set
definitions by predicates was by no means as easy as everybody had
expected. One good example is the small-step relation from Jinja and
its various cousins. It had type ((expr * state) * (expr * state))
set,
Alexander Krauss wrote:
I want to emphasize that the limitation of the code generator mentioned
here not only applies to sets-as-predicates but also to
maps-as-functions and other abstract types that are often specified in
terms of functions (finite maps, almost constant maps, etc.). Thus,
Tobias Nipkow wrote:
Am 12/08/2011 11:27, schrieb Alexander Krauss:
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?
Florian Haftmann wrote:
just do something like (unfold mem_def) and your proof will be a mess
since you have switched to the wrong world.
Like any definition of a primitive operator, mem_def is not really intended
to be unfolded by the user, so don't be surprised if your proof is a mess
after
Quoting Alexander Krauss kra...@in.tum.de:
The same can be done in low-level ML, using just rtac, which
suggests that the error is somewhere in the underlying
Thm.biresolution etc. So far, I have not looked any further...
Hi Alex and Larry,
I guess the culprit is function rename_bvs in
Quoting Lawrence Paulson l...@cam.ac.uk:
But I could be wrong, as such checks may be done elsewhere. Does
anybody else have a suggestion?
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
Quoting Lukas Bulwahn bulw...@in.tum.de:
Hi,
My changes caused this error.
I am working on different compilation schemes in Quickcheck.
Quickcheck registers its type-class based generator construction in the
Datatype package in the HOL image.
Hi Lucas,
according to the trace, the
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
The following datatype specification succeeds as expected
datatype ('a, 'b) foo = Nihil | Bar ('a, 'b) bar
and ('a, 'b) bar = Foo ('a, 'b) foo
whereas the following logically equivalent, but differently written
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
thanks for this offer. But this misperception has not only infected
size but all datatype tools using the
Datatype_Aux.interpret_construction combinator which assumes exactly the
same restriction. Therefore my proposal to
). The above warning was generated by the code for
preprocessing these simplification rules. It should no longer
occur in the current repository version of Isabelle.
Greetings,
Stefan
--
Dr. Stefan Berghofer E-Mail: bergh...@in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
=163589
is still 5.2
Greetings,
Stefan
--
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3Room: 01.11.059
85748 Garching
oops
now yields something like
Counterexample found:
fs = [arbitrary(0 := -1)]
gs = [arbitrary(0 := 0, -1 := 0)]
x = 0
Greetings,
Stefan
--
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische
/RealDef.thy and Real/Rational.thy. Moreover, I modified the setup in such
a way that it also works with the old code generator and therefore with
quickcheck, so the abovementioned bugs should now be fixed.
Greetings,
Stefan
--
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
23 matches
Mail list logo
