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
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 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
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
On 24/09/2018 18:41, Florian Haftmann wrote:
> First-letter abbreviations are not very self-explanatory though. So I'd
> go with something more explicit like »finite_support_fun« – note that
> this type constructor does not show up in concrete type syntax, only in
> type class instantiations, so
Indeed, I am not sure whether avoiding duplication at all cost is what
we should do here. poly_mapping is quite a big thing (and much essential
material is still missing). It was introduced very specifically for the
purpose of building monomials and polynomials. In principle, it can of
course be
I've removed the two rules from continuous_intros as of 1254f3e57fed.
Manuel
On 07/09/2018 14:56, Makarius wrote:
> On 02/09/18 16:00, Manuel Eberl wrote:
>> Okay I did some more experiments and I was now, interestingly enough,
>> completely unable to reproduce the situation wher
I have also noted a few strange issues with the development version
(currently e50312982ba0) these last few days, but I have not yet had the
time to try to reproduce them.
Basically, what happens is that occasionally, the IDE "freezes" in the
sense that no new changes to the document are
gt;
> Makarius
>
>
> On 01/09/18 13:19, Lawrence Paulson wrote:
>> Surely the main issue that blast somehow behaves differently depending upon
>> which machine it’s running on?
>>
>> Larry
>>
>>> On 31 Aug 2018, at 22:35, Makarius wrote:
>
> This thread consists of two sub-threads. The hardware / OS question
> still needs to be sorted out: it might be something with Arch Linux.
I don't really have much of an opportunity to test this on other systems
atm, but I'll see what I can do.
> Apart from that, my reading of blast.ML is that
bit ML
system, and both worked.
Manuel
On 31/08/2018 23:04, Makarius wrote:
> On 31/08/18 22:00, Manuel Eberl wrote:
>>
>> What puzzles me the most is the fact that this behaviour seems to depend
>> on the underlying hardware, and it appears to be 100% reproducible on
>
aded mode).
Perhaps it might also be of interest to try this with different versions
of Poly/ML, just to make sure it's not an issue with the underlying ML
environment.
Manuel
On 31/08/2018 21:53, Makarius wrote:
> On 31/08/18 15:06, Manuel Eberl wrote:
>> Update: I pushed another
to how this kind of
non-deterministic behaviour could come about.
Manuel
On 8/31/18 1:34 AM, Manuel Eberl wrote:
> It seems that my latest commit f443ec10447d causes nontermination of the
> AFP entry "Green".
>
> I saw this timeout on the testboard, but everything worked fin
I had what seems to be a spurious failure of
Probabilistic_Timed_Automata yesterday:
https://ci.isabelle.systems/jenkins/job/testboard/50/consoleFull
The error message is:
*** exception THM 0 raised (line 1136 of "thm.ML"): generalize: bad index
I am quite sure that my (purely cosmetic) changes
I would also have suggested an AFP entry.
> let reflect_along = new_definition
> `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;
Think of it as x being the direction of a ray of light hitting a mirror
(in the shape of a hyperplane through the origin with normal vector a)
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
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
There are definitely books out there that call it the "reflected
polynomial", and that's what my undergraduate discrete maths course
called it, so that's what I called it.
Still, a quick Google search suggests that the terminology you suggest
is more common. I think I'd probably go with
"hg diff" and email it to the other person.
Manuel
>
> Thank you for your help. Let me know when should I should share my
> repository, or if there is a better alternative.
>
> Viorel
>
> -Original Message-
> From: isabelle-dev <isabelle-dev-boun...@mai
Verbose mode ("-v") can sometimes help, because you at least see what
Isabelle is doing.
Another thing you can do is add "-o timeout=600" to your invocation of
isabelle build. Then the build will be stopped after 600 seconds and the
log file might help you identify what theory is causing the
Try -d instead of -D.
The former only specifies a search path for sessions; the second one
additionally tells Isabelle to build all the sessions in that path.
However, we have some high-powered testing hardware here in Munich to
take care of these things, so we can do the testing for you, if you
That /is/ the proper way to test it.
On my machine, HOL-Library takes 6 minutes of CPU time. If it takes
significantly more than that on yours, there's something wrong. If it
takes hours and still isn't done, there's something very wrong.
Are you sure the files are processed fully and without
Oh, well, yes, a special case of metric completion (the reals) was
mentioned in passing, I think. And a more general notion (something like
the completion of a topological group, I think?) featured in my Algebra
1 course, which was an elective. But "metric completion" as such I have
not heard
I for one have not encountered any of these things in my undergraduate
mathematics lectures. But the situation may well be different in other
universities.
On 2018-01-18 15:29, Tobias Nipkow wrote:
> So what is the situation wrt the theories I asked about?
>
> Tobias
>
> On 18/01/2018 15:11,
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
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
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
> 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
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
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
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
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.
>
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
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
)
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
> 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 ...
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
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
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
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
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
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
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
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
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
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
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
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
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 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
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
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:
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!
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
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
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
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
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 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
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 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
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
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
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
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,
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
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
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
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
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
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
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.
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
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:
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
"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
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.
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
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
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
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
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 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
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
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
1 - 100 of 118 matches
Mail list logo
