I came upon a regrssion with the position information in terms that
contain calligraphic or Fraktur letters, e.g.:
theory Scratch
imports Pure
begin
lemma "풜 풜 풜 풜 ()) a b c d e"
The syntax error in this line is at the second closing parenthesis. In
3bfa28b3a5b2, Isabelle/jEdit displays the
I for one almost always do
define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
in such cases, perhaps occasionally combined with a
note [simp] = G_def [symmetric]
at least during the "exploratory" stage of Isar proof writing.
Without that, statements and proof obligations
I don't understand what is going on here. I thought I had to set
ISABELLE_OCAML manually for this kind of code export to even do
something. From what I can tell, I did /not/ set ISABELLE_OCAML on my
machine, but I still get that error. Or did that behaviour change somehow?
Manuel
On 14/03/2019
Hello,
If I'm not mistaken, the default code setup for the "power" operation in
HOL is linear in the exponent (it just does multiplication n times). I
didn't find anything on faster exponentiation in the distribution or the
AFP. so in 154cf64e403e, I committed some material about exponentiation
Hallo,
I just noticed that when exporting code to Haskell, there is a
complication when some of the theories involved have lower-case names.
The code export itself will work with no error or warning, but when
ghc/ghci are invoked on the generated code, they will report the
lower-case module name
Be that as it may, even in that case, I would like the code export tool
to at least output a warning or an error message. Having the code export
tool export produce faulty Haskell code can hardly be intended behaviour.
As an analogy: when I give invalid code to a compiler, I expect it to
complain
Hallo,
partial function in Isabelle are usually modelled as 'a ⇀ 'b, which is
an abbreviation for 'a ⇒ 'b option. There is syntax such as [1 ↦ 2, 3 ↦
4], meaning, basically, λx. if x = 1 then Some 2 else if x = 3 then
Some 4 else None. There is also update syntax for such function, such
as f(1 ↦
Hallo,
The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
interface Fun_Cases.fun_cases.
What do you mean by that? There exists an ML function
Fun_Cases.mk_fun_cases : Proof.context - term - thm -- is that not an
ML interface to the Fun_Cases tool? Or do you also want a
Hallo,
I am not, as it were, a user of Proof General anymore; however, I would
like, if I may, to point out one thing that annoys me in jEdit and that
was, in my opinion, better in Proof General: the handling of
abbreviations for Unicode characters.
The current behaviour with “immediate
types are “natural” codatatypes, so defining
them as datatypes makes everything a bit more clumsy.
Cheers,
Manuel Eberl
On 07.05.2014 16:50, Makarius wrote:
On Wed, 7 May 2014, Johannes Hölzl wrote:
* Theorems about complex numbers are now stated only using Re and Im,
the Complex
constructor
Yes, but the underlying reason for that is that complex numbers are
isomorphic to pairs of real numbers, and binary product types are
degenerate (I would rather say very basic) co-algebraic datatypes.
So my point (and I would guess Andrei's as well) is that this really has
nothing to do with
I am not terribly happy about that. I use approximation of powr in my work on
Akra–Bazzi and the Master theorem.
I take it that a powr b = exp (ln a * b) still holds for positive a. I could
probably apply that rewrite rule before applying approximation, but it would of
course be nice if I did
Hallo,
thanks for all the good work. It's nice to finally see my work
integrated so neatly into HOL.
1. Normalization. Currently, there is normalization_factor such that a
div normalization_factor a yields the normalized elements. My impression
is that the latter should be an operation on
On 24/06/15 15:55, Larry Paulson wrote:
A more appropriate point is that it can be tricky in Isabelle/jEdit to
determine the type of an expression such as “of_nat k”, as there is nothing to
click on.
When I type ‘term sqrt (of_nat 2)’ and hover over the ‘of_nat’, it
says ‘constant
.
declare [[coercion of_nat :: nat ⇒ real]]
term sqrt (2 :: nat)
Today the output says sqrt (real_of_nat 2). But if there would be no
abbreviation for of_nat :: nat ⇒ real, how would you deduce the type
of the coercion.
Dmitriy
On 24.06.2015 16:01, Manuel Eberl wrote:
On 24/06/15 15:55, Larry
On 27/06/15 09:06, Florian Haftmann wrote:
What about: »a = unit_factor a * normalize a«
Sounds reasonable.
I still had the hope that it would be possible to develop an abstract
specification for gcd which would form a lattice: »gcd a a = a«. But
now I cam to realize that for Gcd :: 'a set =
I also vote for b). I would also like to add that I ran into situations
where I required the notation of an inverse element in a ring. I defined
this as ring_inv x = 1 div x. For instance, on int, we have ring_inv
1 = 1 and ring_inv (-1) = -1 and everything else is basically
ill-defined, because 1
I think the main (and only) problem is that it uses significantly more
memory.
On 28/05/15 11:21, Peter Lammich wrote:
Hi list,
When I start Isabelle, I get the following warning message on the
console:
### Cannot execute Poly/ML in 32bit mode (missing shared libraries for
C/C++)
### Using
Ah, interesting. Thanks!
On 23/09/15 08:47, Andreas Lochbihler wrote:
> Dear Manuel,
>
> consider supports the same syntax as obtains, i.e., you can use "where"
> as in
>
> consider "x = ∞" | "x = -∞" | y where "x = ereal y&quo
I completed the merge I mentioned in my previous email. Everything went
into Multivariate_Analysis, apart form Nonpos_Ints and Periodic_Fun,
which went into Library.
I'm running tests overnight to make sure I did not break anything.
Manuel
On 01/01/16 20:50, Manuel Eberl wrote:
I still
I still have a few thousand lines of stuff to merge into the
distribution, most notably the definition of the radius of convergence
of a series and a number of convergence tests.
This would be nice to have in the distribution because two results of
mathematical importance rest upon it: the
Ah yes, I completely forgot about that. Will do.
On 05/01/16 14:27, Makarius wrote:
On Mon, 4 Jan 2016, Manuel Eberl wrote:
I completed the merge I mentioned in my previous email.
Fine. This is Isabelle/b0f941e207cf.
Do you want to write an entry for NEWS and CONTRIBUTORS?
Makarius
This particular issue has, in fact, annoyed me a great deal. I needed
the ‘dist_norm’ lemma a lot lately and was never able to find it with
‘find_theorems’, which was very frustrating. I eventually found it by
reading a proof that used it somewhere.
I did not think much of it at the time, but
Lars just informed me that I didn't actually include an example in my
mail (I thought I did); it was therefore probably not clear what I meant
exactly, so let me explain:
When I write "\ci" in a theory, it used to be completed to ∘
immediately. As of 1ca11ddfcc70, this does not happen
As of the following revision, immediate completion does not work anymore
in Isabelle/JEdit:
changeset: 61600:1ca11ddfcc70
user:wenzelm
date:Sat Nov 07 16:05:28 2015 +0100
summary: clarified completion of explicit symbols (see also
f6bd97a587b7, e0e4ac981cf1);
From the
I already moved a few small lemmas. I also defined the notion of an
algebraic number; as soon as your AFP entry works with the development
version of Isabelle again (is that already the case?), I will prove
equivalence of my definition in Poly_Deriv.thy to your definition in
Algebraic_Numbers
I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
algebraic number.
Oh, yes, you're right. It's in
https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
.
Its definitely not optimal, and
I tried to trace this issue and I am really confused now.
The problem is apparently the following code equation I added for
"binomial" at the end of Binomial.thy:
lemma binomial_code [code]:
"(n choose k) =
(if k > n then 0
else if 2 * k > n then (n choose (n - k))
else
I already have Sturm_Tarski running again and will commit that later today.
On a related note, in faf1aa9381e0, I also removed the definition of
"algebraic" from Algebraic_Numbers and updated it to use the more
general definition of "algebraic" that is now in the library.
Cheers,
Manuel
There are actually several affected functions:
Discrete.sqrt
size_fset
lapprox_posrat
size_multiset
set_encode
card_UNIV_fun
card_UNIV_set
card_UNIV_finfun
I have no idea what causes this and why my changed affected it. I also
do not have the faintest idea what I could possibly do to fix it.
I commented out the code equation in question and HOL-Codegenerator_Test
runs through again.
Manuel
On 12/01/16 15:31, Makarius wrote:
On Tue, 12 Jan 2016, Manuel Eberl wrote:
From what I have seen so far, it seems like there are some lingering
issues with code generation in general
ave compared it with the MyRat implementation by Manuel Eberl
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg2.html
as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski
b11e8139b880 (where a comment says that it goes back to John Harrison).
Further comments? Anyt
Florian has already hinted at it, but I will say it again explicitly:
Mathematically, gcd and lcm are not operations on the elements of a
ring, but on the equivalence classes w.r.t. associatedness (i.e. mutual
divisibility). In fact, these equivalence classes form a complete
lattice w.r.t.
om of these problems!
All of these texts were copied from HOL Light. I can fix them sometime
tomorrow, or feel free to do it yourself if you prefer.
--lcp
On 15 Jun 2016, at 21:17, Manuel Eberl <ebe...@in.tum.de> wrote:
There is one instance in Extension.thy where you wrote "real ^ n&
There is one instance in Extension.thy where you wrote "real ^ n" in a
subsection heading about Urysohn's lemma. That causes an error when
interpreted as LaTeX code. I suggest replacing it with "Euclidean
space", which is more apt in Isabelle anyway, I should think.
There are two more
This is my entry. I submitted it a few days ago, and I included the
config file in my submission. I was not aware that those don't exist
anymore.
On 23/06/16 09:49, Florian Haftmann wrote:
Dear AFP maintainers,
in 79fb78da1ef0 there exists exactly one file named "config", namely
The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used
to break Codegenerator_Test. I can have a look later to see whether this
is still the case.
If it is not, we should probably proceed to move some more of René
Thiemann et al's efficient code equations from the AFP to the
Looks good. After applying the patch, HOL-Codegenerator_Test goes
through with the code equation in Binomial.thy enabled.
Cheers,
Manuel
On 23/06/16 09:48, Manuel Eberl wrote:
The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used
to break Codegenerator_Test. I can have
Florian, what are you plans w.r.t. merging this patch into the distribution?
Manuel
On 23/06/16 11:22, Manuel Eberl wrote:
Looks good. After applying the patch, HOL-Codegenerator_Test goes
through with the code equation in Binomial.thy enabled.
Cheers,
Manuel
On 23/06/16 09:48, Manuel
I added the efficient code equations for fact and binomial, and similar
ones for pochhammer and gbinomial.
I also adapted everything from Square_Free_Factorization and
Missing_Polynomial that seemed to be of general interest to me
(especially the generalisation of the type of pderiv).
I
It looks like I'm the one who broke it. It does not work after my commit
3201ddb00097, but it still works in Fabian's d8e7738bd2e9 immediately
before.
I have no idea what causes this problem. Maybe one of our resident code
generator experts could comment on it?
I'll try to find out which
As of 67792e4a5486, I fixed a regression in the ‘approximation’ decision
procedure that was introduced with Isabelle2015: approximating terms
containing ‘powr’ did not work anymore due to the changed definition of
‘powr’.
It works again now and I was wondering whether this kind of thing
ed entries are in dire need of a major
cleanup. Echelon_Form/Rings2 in particular contains a lot of interesting
material.
Cheers,
Manuel
On 28/02/16 15:45, Lawrence Paulson wrote:
Looks like valuable work even if it caused some disruption.
Larry
On 28 Feb 2016, at 13:32, Manuel Eberl <ebe...@in.
"multiplicity" is definitely interesting; we could then probably define
the "order" of a root of a polynomial in terms of "multiplicity", which
simplifies things a bit.
I don't see why is_prime should require an algebraic_semidom; the
definition of prime elements makes sense in any
ith Euclidean
rings) in a way that works well in practice and see where that leads us.
Manuel
On 11/03/16 13:39, Tjark Weber wrote:
Florian,
On Thu, 2016-03-10 at 14:01 +0100, Manuel Eberl wrote:
"multiplicity" is definitely interesting [...]
I don't see why is_prime shoul
Argh! You are correct. Today is /not/ my day. I'm on it.
On 24/05/16 18:42, Makarius wrote:
On 24/05/16 18:34, Manuel Eberl wrote:
I'm confident that I'll have everyting up and running again soon.
BTW, current Isabelle/8230358fab88 now looks like too much has been
committed
Yes, this was my fault. The problem was that I stupidly forgot to commit
my changes before I pushed to the testboard and thus did not see the
problems caused by my changes.
I'm confident that I'll have everyting up and running again soon.
Manuel
On 24/05/16 17:22, Jasmin Blanchette wrote:
I've been using multisets quite a bit myself lately. add# and add1# both
sound all right to me.
I would also like to point out that for some reason, intersection and
union are #∪ and #∩, whereas all other multiset operations seem to have
the # at the end (e.g. ⊆#). Unless there is some deeper
Yes, that might be a good idea.
On 27/07/16 11:24, Tobias Nipkow wrote:
Naming: can't we drop "is_"?
Tobias
On 27/07/2016 10:46, Manuel Eberl wrote:
*** HOL ***
* Number_Theory: algebraic foundation for primes: Introduction of
predicates "is_prime", "irreducible
But is it possible to adapt all lemmas accordingly? I could imagine
that some statements use the fact that the support of multiplicity are
the prime numbers.
Not really. Some facts will still require the primality assumption, e.g.
lemma prime_multiplicity_mult_distrib:
assumes "is_prime_elem
Hallo,
as some of you may already know, I am currently in the process of
resructing Isabelle's definitions of prime numbers. Before these
changes, we had the concept of "multiplicity". This was defined to be
the multiplicity of a prime factor in the prime decomposition of a
natural number or
sure that there is no standard definition of this concept in
mathematics that we should follow?
Tobias
On 19/07/2016 12:03, Manuel Eberl wrote:
Hallo,
as some of you may already know, I am currently in the process of
resructing
Isabelle's definitions of prime numbers. Before these changes, we ha
Hallo,
sorry for the broken AFP – it's my fault, but I added a lot of new
material about rings and prime factor decomposition. The projects that
were affected by this the most are already fixed, and I will take care
of the rest on Monday.
Manuel
I've heard of negative thermal expansion in some materials, but I don't
think RAM is subject to it. (scnr)
In a more serious fashion: I don't see how ambient temperature could
affect memory usage. I've run into "insufficient memory" and stack
overflow problems in Isabelle several times
I'm not an expert in complex analysis either, but do remember that it
was briefly mentioned – but not proved – in my introductory lecture on
Complex Analysis when I was an undergratuate.
My intuition tells me that this is a very beautiful result, but not one
that you need a lot, but I could be
The desired multi-variable semantics of ∄ seem obvious enough to me and
I think that this should be allowed.
For ∃!, the implicit complexity introduced by the pairing seems too much
to me, so I think this should be forbidden.
On 13/09/16 10:41, Johannes Hölzl wrote:
There is even a third
I've never used SourceTree, and it is, of course, very difficult to
debug such things from afar.
I could of course, with your permission, simply commit and push the
entry myself.
Cheers,
Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Oh, that is quite possible. Sorry about that. I typically keep my
prospective AFP entries in private HG repositories and then simply
tarball and submit them when it's time. I don't think that ever was a
problem before, but it sounds like the most reasonably explanation so far.
Good catch!
Hallo,
I've been playing around with corec and friends in combination with the
lazy lists from "$AFP/Coinductive/Coinductive_List" and encountered the
following problem:
Suppose I want a function that takes two (implicitly sorted) lazy lists
and merges them in the following fashion:
I have decided to add my own opinions to this debate. My knowledge of
the old testing system is limited, but I hope my perspective will still
hold some interest.
First of all, a usable testing infrastructure does not grow overnight by
itself. Someone has to put in a lot of time and effort to make
This is a problem that I have given quite some thought in the past. The
problem is the following: You have a theory A providing certain
operations on sets (in this case: Gcd) and a theory B providing
implementations for sets (in this case: Containers).
The problem is that the code equations for
are done at all at
> the moment.
>
> Manuel's suggestion of code_abort is a bit cleaner than René's use
> Code.abort, because Code.abort does not work with normalisation by
> evaluation whereas code_abort does.
>
> Best,
> Andreas
>
>
> On 03/10/16 15:29
This, too, is an industry standard. Of course, I am not the expert, but
I'm pretty sure this is achievable with the system we have – if there is
a consensus that this is what we want, that is.
Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
lt value is that the
> finiteness test remains inside the implementation library B whereas with
> Finite_Set.fold, the finiteness test must be done whenever one wants to
> use the combinator. So this might be an argument in favour of fold_default.
>
> Andreas
>
> On 03/1
I am glad to announce that as of261d42f0bfac, Old_Number_Theory is
finally history.
A lot of the proofs are still quite messy and don't take advantage of
the new features we now have in Number_Theory (such as a uniform concept
of ‘primes’ and ‘prime factorisations’ for both nat and int), but
One remark on the diff:
+ src/HOL/Number_Theory/QuadraticReciprocity.thy
+ src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
This is a formal regression: a proper name has turned into CaMlCaSe.
But that should be easy to correct.
Ah indeed. Jaime probably didn't know about the naming
with what we have for analysis. I blame John Harrison :-)
Larry
On 18 Oct 2016, at 12:11, Manuel Eberl <ebe...@in.tum.de
<mailto:ebe...@in.tum.de>> wrote:
I am glad to announce that as of261d42f0bfac, Old_Number_Theory is
finally history.
A lot of the proofs are still quite mes
I for one am hoping to be able to get rid of the Old Number Theory
before the release. All that is left to do is actually to adapt some
theories of the ported theories to my recent changes concerning prime
numbers, so I think I should be able to take care of that next week.
Cheers,
Manuel
On
During a minor overhaul of some theories in the distribution, I
discovered some problems with theory imports.
Apparently, the theory merge behaviour changed in one of the most recent
commits. I haven't been able to pin down which one it is exactly; I
might do a bisection later if needed.
In
There was an odd error in a testboard-afp job [1] before:
17:26:32 ### Ignoring bad database:
"$ISABELLE_HOME/heaps/$ML_IDENTIFIER/log/HOL-Library.db"
17:26:32 ### [SQLITE_ERROR] SQL error or missing database (no such
table: isabelle_session_info)
[…]
17:32:12 *** [SQLITE_ERROR] SQL error or
On 2017-07-05 22:09, Manuel Eberl wrote:
> I still want to take care of two really tiny things: […] and the proper
> printing
> of "nat" values as numerals instead of successor notation.
This is now done as of adf3155c57e2. I should note that I was somewhat
imprecise, b
me reasonably large n.
>
> Cheers,
> René
>
> PS: Unfortunately, Sqrt_Babylonian.log_floor and log_ceiling are not
> connected to Discrete.log.
>
>> Am 29.06.2017 um 15:29 schrieb Manuel Eberl <ebe...@in.tum.de>:
>>
>> Hallo,
>>
>> I'm
omplex_Main think
about that.
Manuel
On 2017-06-30 16:52, Tobias Nipkow wrote:
>
> On 30/06/2017 16:39, Manuel Eberl wrote:
>> I do understand that argument, but I am not sure if
>> Topological_Spaces.subseq is really used /that/ often. Actually,
>> going one step furth
On 2017-06-30 20:33, Sebastien Gouezel wrote:
> I used subseq quite heavily in my ergodic theory developments. From
> a mathematician point of view, taking subsequences of sequences
> from nat to nat is very common and very useful in analysis (much
> more than taking subsequences of lists).
So
ymbol.
> It would be nice if non-quaified names could be found for this case.
>
> Tobias
>
> On 30/06/2017 16:14, Lawrence Paulson wrote:
>> Indeed we do.
>> Larry
>>
>>> On 28 Jun 2017, at 18:49, Manuel
Hallo,
I'm considering adding efficient code for Discrete.log (the dual
logarithm on natural numbers). PolyML does provide an IntInf.log2
function that seems reasonably efficient so that one can set up code
printing. However, I am struggling with one detail:
Where would the code that does this
Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.
If anybody has better suggestions, I am open to implementing them.
Manuel
On 2017-06-28 17:05, Andreas Lochbihler wrote:
> Dear all,
>
> While porting some of my theories to the current
code_post rules to rewrite
successor notation to numerals is a lot better than what we have at the
moment.
Manuel
On 2017-07-05 21:45, Lawrence Paulson wrote:
> What’s the idea here?
> Larry
>
>> On 5 Jul 2017, at 21:09, Manuel Eberl <ebe...@in.tum.de> wrote:
>>
>
I still want to take care of two really tiny things: the "subseq"
situation and the proper printing of "nat" values as numerals instead of
successor notation.
Just mentioning that for the sake of completeness.
Manuel
On 2017-07-05 21:04, Makarius wrote:
> Dear all,
>
> we are now almost 7
Before I forget: I did that and it is as expected; everything still works.
Manuel
On 2017-04-25 11:12, Florian Haftmann wrote:
Am 25.04.2017 um 11:06 schrieb Manuel Eberl:
I think you actually solved that problem by now. If I recall correctly,
it was one of the two dictionary-related
Hallo,
I just had a strange build failure with HOL-Probability. I executed
manuel@colosson ~/.i/etc> isabelle-dev build -d '$AFP' Random_BSTs
Euler_MacLaurin Bertrands_Postulate
and HOL-Probability failed to build:
Building HOL-Probability ...
HOL-Probability FAILED
(see also
I think you actually solved that problem by now. If I recall correctly,
it was one of the two dictionary-related problems I told you about a
year ago or so, and then Lars and you solved that problem somehow.
I can try putting in that code equation again and seeing what happens.
>> (*TODO: This
Hallo,
on 158c513a39f5, I just had a JVM crash during "isabelle build" when it
was building Isabelle/Scala. (Log attached).
When I did "isabelle build" again, it proceeded to build the Pure
session without problems. However, when I then tried to build
HOL-Computational_Algebra, it stopped and
The following seems to be the most reliable way to trigger the problem:
while true
isabelle build -b -c Pure
end
I did that and about 6% of builds with Scala 2.12.3 failed with
something like the attached log. I then tried the same thing with Scala
2.12.2 (double-checked "isabelle scala
That was due to my reforms of the sublist/subseq stuff and should be
repaired by this afternoon. Tomorrow's slow tests should run through
fine again. Unfortunately, these slow sessions don't have the same rapid
testing cycle as the normal sessions.
Manuel
On 2017-06-01 16:19, Florian
On 2017-08-24 17:34, Florian Haftmann wrote:
> I would still appreciate if someone would take the comment »Deviates
> from the definition given in the library in number theory« as a starting
> point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.
Oh actually I fixed that a
Purely out of interest: Does this also hold for filters?
Manuel
On 2017-08-24 20:54, Viorel Preoteasa wrote:
> I have now a file with the new class, and all necessary proofs
> (both distributivity equalities, bool, set, fun interpretations,
> proofs of the old distributivity properties).
>
> I
> If you still have that, can you send it to me?
Sure.
> Since the JVM crash happened during scalac compilation, I recommend to
> enforce a fresh build, e.g. like this:
That seems to have worked. The only output I got was this:
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
)
So, all in all, my money would be on the JVM.
Manuel
On 19/08/17 21:04, Makarius wrote:
> On 19/08/17 20:31, Manuel Eberl wrote:
>>> If you still have that, can you send it to me?
>>
>> Sure.
>>
>>> Since the JVM crash happened during scalac compilation, I
Okay I have no idea what is going on anymore.
I know have the following new data points:
– 2500 iterations on my Intel Core i7 laptop. No failures.
So it must be the Ryzen issue after all, I thought. I recalled that some
people said the problem was less pronounced with SMT disabled, so I
that solved whatever issue I was having, and, of course, it took a
reboot for it to kick in.
On 20/08/17 14:14, Manuel Eberl wrote:
> Okay I have no idea what is going on anymore.
>
> I know have the following new data points:
> – 2500 iterations on my Intel Core i7 laptop. No failures.
>
kernel within the last few
> weeks that solved whatever issue I was having, and, of course, it took a
> reboot for it to kick in.
>
> On 20/08/17 14:14, Manuel Eberl wrote:
>> Okay I have no idea what is going on anymore.
>>
>> I know have the following new data poi
Is it intentional that the "Computational_Algebra" theory does not
import "Polynomial_Factorial"?
Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
to make it considerably less frequent; however, only in Poly/ML 5.7.1
does it appear to not happen at all no matter how I run it.
Does Poly/ML 5.7.1 contain any changes that could plausibly cause this
bad behaviour to go away?
Manuel
On 2017-11-07 09:51, Manuel Eberl wrote:
> It seems l
> If these crashes are happening at the end of the build process I would
> suspect that it is something to do with either the data sharing or
> writing out the heap image.
Does writing out of the heap happen also when I just do "isabelle build
Pure" as opposed to "isabelle build -b Pure"? Because
If there are fixed-size integers in ML that raise an exception on
overflow, it should be possible to just do appropriate code_printing
setup similar to what Code_Target_Numeral does. We already have to
somehow magically map Isabelle's "int" type to ML's "IntInf" type, so
all we have to do is to
Is there an easy way to disable that for testing purposes? Some line I
have to remove from a .scala file or something?
Manuel
On 2017-11-08 15:44, Makarius wrote:
> On 08/11/17 15:39, Manuel Eberl wrote:
>>> If these crashes are happening at the end of the build process I would
017-11-08 15:35, Makarius wrote:
> On 08/11/17 09:21, Manuel Eberl wrote:
>> After a lengthy bisection, I found that the first revision where no
>> crashes occur is this one:
>>
>> changeset: 66920:aefaaef29c58
>> user: wenzelm
>> date: Thu O
I have a student who was going to formalise things about fields and
field extensions. Does that clash with your work in any way?
In any case, we should definitely coordinate our efforts here to avoid
duplication of work.
Manuel
On 2018-05-08 13:49, Lawrence Paulson wrote:
> I have two interns
It works fine for me.
Did you perhaps switch on ML debugging/exception tracing? HOL becomes
virtually impossible to build with that switched on. What is the content
of your ".isabelle/etc/preferences"?
Manuel
On 2018-05-21 15:43, Lawrence Paulson wrote:
> I am continuing to be plagued by HOL
1 - 100 of 118 matches
Mail list logo
