Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Manuel Eberl]

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 15:24, Lars Hupel wrote:
>> I get this failure on my regular Ubuntu 18.04:
>>
>> *** Failed to load theory "HOL-Library.Library" (unresolved
>> "HOL-Library.Finite_Map")
>> *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec"
>> ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
>> *** At command "export_code" (line 1428 of
>> "~~/src/HOL/Library/Finite_Map.thy")
> Same error also on Jenkins.
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] infix line breaking

[Manuel Eberl]

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 in HOL-Algebra become
totally unreadable in my experience.

Manuel


On 22/02/2019 17:20, Lawrence Paulson wrote:
> The pretty printing of infix operators looks pretty terrible in the presence 
> of large terms.
>
> I’d like to propose having infix operators breaking at the start of the line 
> rather than at the end. Any thoughts?
>
> Larry
>
> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) 
> {pp}) {} (nsphere 0) {} r
>d =
> hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>  (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 
> 0) {nn}) {} r
>(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Wrong position information in 3bfa28b3a5b2

[Manuel Eberl]

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 error at the space between "a"
and "b". Clicking anywhere after the initial "풜" also leads to the
caret being put too far to the left. Each "풜" seems to shift the offset
further, so I guess there's an off-by-one error in there somewhere.
Interestingly, not all letters cause this – e.g. "ℳ" seems to be fine.

In Isabelle 2018, everything works as expected. I do not have the time
to do a bisection right now, but I can do one if it helps.

Cheers,

Manuel


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Exponentiation by squaring

[Manuel Eberl]

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
by squaring that works in logarithmic time in the exponent for monoid_mult.

I wonder if this should be a code_unfold or code_abbrev rule for
monoid_mult in general, or perhaps just for some instances like nat and int.

There's also setup in HOL-Number_Theory to do modular exponentiation "a
^ n mod m" and congruences of the form "[a ^ n = b] (mod m)" using this,
at least for int and nat. I'm not sure if the rules I set up are the
best ones and, again, this could be generalised to
euclidean_semiring_cancel but I'm not sure if I should.

Does anyone have any stakes in/opinions on this?

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Frag / Poly_Mapping

[Manuel Eberl]

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 its length should be fine.

It does show up in the name of the operations you define on it and the
theorems you prove about it though.

Manuel



pEpkey.asc
Description: application/pgp-keys
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Frag / Poly_Mapping

[Manuel Eberl]

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 seen in a much more general light. On the other hand, the free
abelian groups have a more narrow focus.

Now, we could implement free abelian groups with poly_mapping. What
would that entail? We would have to move it to the distribution, but
then I think we should then also attempt to really clean it up quite a
bit. Also, we would need to rename it to something catchy and more
general. "Function with finite support" is what it essentially is, so
perhaps "fsfun"?

Also, any changes that we make will have repercussions in the AFP and
possibly other non-AFP applications (I'm concerned about IsaFoR in
particular, so I cc'ed René).

Manuel


On 24/09/2018 16:32, Lawrence Paulson wrote:
>> On 24 Sep 2018, at 10:30, Alexander Maletzky 
>>  wrote:
>>
>> Some notions defined in "Frag.thy" already exist in "Poly_Mapping.thy": 
>> "support" is called "keys" there, and I think "frag_cmul" could easily be 
>> defined in terms of "map".
>>
>> "frag_extend" looks like a special case of a more general subsitution 
>> homomorphism "subst" of type "('a => 'b => 'c) => ('a =>_0 'b) => 'c", 
>> defined as "subst f x = (\Sum i\in keys x. f i (lookup x i))", which could 
>> indeed be added to "Poly_Mapping.thy". The insertion morphism in 
>> "MPoly_Type.thy" could then perhaps be defined in terms of "subst" (at least 
>> partially; for power-products, the above sum would have to be replaced by a 
>> product).
> Thanks for that. Manuel is expressing the opposite point of view, namely that 
> it might be better to keep the two developments 100% separate. Certainly the 
> basic setup of Frag is simple and short (see below) and we don't have to 
> concern ourselves with how Poly_Mapping is used by other developments in the 
> AFP and in other projects outside. So I'm puzzled as to the best course.
>
> Larry
>
> typedef 'a frag = "{f::'a\int. finite {x. f x \ 0}}"
>   by (rule exI [where x = "\x. 0"]) auto
>
> definition support 
>   where "support F = {a. Rep_frag F a \ 0}"
>
> declare Rep_frag_inverse [simp] Abs_frag_inverse [simp]
>
>
> instantiation frag :: (type)comm_monoid_add
> begin
>
> definition zero_frag_def: "0 \ Abs_frag (\x. 0)"
>
> definition add_frag_def: "a+b \ Abs_frag (\x. Rep_frag a x + 
> Rep_frag b x)"
>
> lemma finite_add_nonzero: "finite {x. Rep_frag a x + Rep_frag b x \ 0}"
> proof -
>   have "finite {x. Rep_frag a x \ 0}" "finite {x. Rep_frag b x 
> \ 0}"
> using Rep_frag by auto
>   moreover have "{x. Rep_frag a x + Rep_frag b x \ 0} \ {x. 
> Rep_frag a x \ 0} \ {x. Rep_frag b x \ 0}"
> by auto
>   ultimately show ?thesis
> using infinite_super by blast
> qed
>
> lemma finite_minus_nonzero: "finite {x. - Rep_frag a x \ 0}"
>   using Rep_frag [of a] by simp
>
> instance 
> proof
>   fix a b c :: "'a frag"
>   show "a + b + c = a + (b + c)"
> by (simp add: add_frag_def finite_add_nonzero add.assoc)
> next
>   fix a b :: "'a frag"
>   show "a + b = b + a"
> by (simp add: add_frag_def add.commute)
> next
>   fix a :: "'a frag"
>   show "0 + a = a"
> by (simp add: add_frag_def zero_frag_def)
> qed
>
> end
>
> instantiation frag :: (type)ab_group_add
> begin
>
> definition minus_frag_def: "-a \ Abs_frag (\x. - Rep_frag a x)"
>
> definition diff_frag_def: "a-b \ a + - (b::'a frag)"
>
> instance 
> proof
>   fix a :: "'a frag"
>   show "- a + a = 0"
> using finite_minus_nonzero [of a]
> by (simp add: minus_frag_def add_frag_def zero_frag_def)
> qed (simp add: diff_frag_def)
>
> end
>
>
> definition frag_of where "frag_of c = Abs_frag (\a. if a = c then 1 
> else 0)"
>
> lemma frag_of_nonzero [simp]: "frag_of a \ 0"
> proof -
>   have "(\x. if x = a then 1 else 0) \ (\x. 0::int)"
> by (auto simp: fun_eq_iff)
>   then have "Rep_frag (Abs_frag (\aa. if aa = a then 1 else 0)) 
> \ Rep_frag (Abs_frag (\x. 0))"
> by simp
>   then show ?thesis
> unfolding zero_frag_def frag_of_def Rep_frag_inject .
> qed
>
> definition frag_cmul :: "int \ 'a frag \ 'a frag"
>   where "frag_cmul c a = Abs_frag (\x. c * Rep_frag a x)"
>
>


pEpkey.asc
Description: application/pgp-keys
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

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 where Green /didn't/
>> timeout. So I have no idea what was going on there; perhaps I made a
>> mistake in testing it. I don't know.
>>
>> It might be wise to remove "continuous_on_discrete" etc. from
>> intro/continuous_intros and declare it as a simp rule instead. I'm still
>> not quite sure what causes these problems.
> The official isabelle-dev test results show that Ergodic_Theory and Lp
> have suffered a lot:
>
> https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Ergodic_Theory
> https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Lp
>
>
> Here are some manual measurements:
>
> Isabelle/9207ada0ca31 + AFP/6d7e0f6b8096
> Finished HOL (0:03:18 elapsed time, 0:11:01 cpu time, factor 3.33)
> Finished HOL-Analysis (0:05:44 elapsed time, 0:26:07 cpu time, factor 4.55)
> Finished HOL-Probability (0:01:15 elapsed time, 0:05:25 cpu time, factor
> 4.30)
> Finished Lp (0:00:15 elapsed time, 0:01:03 cpu time, factor 4.21)
>
> Isabelle/f443ec10447d + AFP/6d7e0f6b8096
> Finished HOL (0:03:19 elapsed time, 0:11:03 cpu time, factor 3.33)
> Finished HOL-Analysis (0:05:58 elapsed time, 0:27:06 cpu time, factor 4.54)
> Finished HOL-Probability (0:01:16 elapsed time, 0:05:24 cpu time, factor
> 4.22)
> Finished Lp (0:02:41 elapsed time, 0:03:42 cpu time, factor 1.38)
>
>
> So it is probably better to revise the rule declarations in main HOL.
>
>
>   Makarius


pEpkey.asc
Description: application/pgp-keys
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Manuel Eberl]

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 processed. I can still
view the output of all the processed commands, but there is a certain
position in the document underneath which all the text is red, and it
never because not red. If I change anything in the text before that, it
also becomes red forever.

It seems to me that this is particularly triggered by non-terminating
invocations of simp/auto/etc., even if I abort them after a fraction of
a second.

I don't think the 2018 release had this problem, but I could be wrong.

If I find out any more precise details, I will let you know.

Manuel


On 07/09/2018 17:39, Lawrence Paulson wrote:
> What do you suggest for these on a 16 GB machine? I attach my file.
> Larry
>
>> On 7 Sep 2018, at 15:01, Makarius > > wrote:
>>
>> If you are using the 64-bit version of Poly/ML, you should give both
>> --minheap and --maxheap, otherwise it tends to overcommit a lot of
>> memory.
>
>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


pEpkey.asc
Description: application/pgp-keys
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

Okay I did some more experiments and I was now, interestingly enough,
completely unable to reproduce the situation where Green /didn't/
timeout. So I have no idea what was going on there; perhaps I made a
mistake in testing it. I don't know.

It might be wise to remove "continuous_on_discrete" etc. from
intro/continuous_intros and declare it as a simp rule instead. I'm still
not quite sure what causes these problems. I attached a log of blast
with "blast_trace" enabled.

Manuel

On 01/09/2018 14:20, 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.
>
> Apart from that, my reading of blast.ML is that the "continuous_on" rule
> is applied in the search independently of its fine-grained type
> information. Is that correct?
>
>
>   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:
>>>
>>> On 31/08/18 22:00, Manuel Eberl wrote:
>>>> That's interesting. I suspected one of the "continuous_on" rules would
>>>> be the cause. In any case, I don't know how the unification works
>>>> exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
>>>> apply to this goal at all due to its restrictive type class constraint.
>>> Blast does its own unification, without taking fully account of types
>>> and type classes. The found proof is then reconstructed as in "fast" and
>>> its friends, using regular Isabelle term + type unification.
>>>
>>> Larry should be able to say more precisely, what the limits of blast are.
 [0]  
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) 
C1_differentiable_on S - Sa)) :: bool ⇒ bool 
branch split: 2 new subgoals 
+ 
 [0]  
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool 
moving formula to unsafe list 
+ 
 [0]  
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool  (Unsafe) 
Limit reached. 
Backtracking; now there are 1 branches 
Backtracking; now there are 1 branches 
 [1]  
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) 
C1_differentiable_on S - Sa)) :: bool ⇒ bool 
branch split: 2 new subgoals 
+ 
 [1]  
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool 
moving formula to unsafe list 
+ 
 [1]  
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool  (Unsafe) 
branch closed by rule 
 (duplicating) 
 [1]  
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool 
moving formula to unsafe list 
 [1]  
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool  
(Unsafe) 
branch extended (1 new subgoal) 
 (duplicating) 
 [0]  
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool 
branch split: 2 new subgoals 
+ 
 [0]  
¬ finite ?var :: bool ⇒ bool 
branch closed by rule 
 1 variable UPDATED: 
   set_mset ?var 
 [0]  
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool 
moving formula to literals 
 [0]  
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool  
(Unsafe) 
Limit reached. 
Backtracking; now there are 2 branches 
branch closed by rule 
 1 variable UPDATED: 
   set ?var 
 [0]  
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool 
moving formula to literals 
 [0]  
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool  
(Unsafe) 
Limit reached. 
Backtracking; now there are 2 branches 
branch closed by rule 
 1 variable UPDATED: 
   bot 
 [0]  
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool 
moving formula to literals 
 [0]  
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool  
(Unsafe) 
Limit reached. 
Backtracking; now there are 2 branches 
branch extended (1 new subgoal) 
 1 variable UPDATED: 
   ?var - insert ?var ?var 
Excessive branching: KILLED 
moving formula to unsafe list 
+ 
 [0]  
¬ finite ?var :: bool ⇒ bool  (Unsafe) 
Limit reached. 
Backtracking; now there are 1 branches 
Backtracking; now there are 1 branches 
Backtracking; now there are 2 branches 
Backtracking; now there are 1 branches 
Backtracking; now there are 1 branches 
 [2]  
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) 
C1_differentiable_on S - Sa)) :: bool ⇒ bool 
branch split: 2 new subgoals 
+ 
 [2]  
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool 
moving formula to unsafe list 
+ 
 [2]  
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool  (Unsafe) 
branch closed by rule 
 (duplicating) 
 [2]  
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool 
moving formula to unsafe list 

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

> 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 the "continuous_on" rule
> is applied in the search independently of its fine-grained type
> information. Is that correct?

Even if it is, it has no preconditions, so I don't see how it could
cause nontermination.

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

It works on both my work laptop and my private desktop PC.

The work laptop is an Intel i7 something (I cannot recall the exact
model off the top of my head) and the desktop is an AMD Ryzen 1800X.
Both run with an up-to-date Arch Linux.

At least on the desktop, I tried it with both the 32 and 64 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
>> machines where it does happen. If this is a race condition, it must be
>> one of the strangest one I have ever seen (note that it even happens in
>> single-threaded 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.
> 
> I see the same effect with Poly/ML 5.6 from Isabelle2017: a quite
> different environment compared to Isabelle2018.
> 
> It requires the included change, and the following in
> $ISABELLE_HOME_USER/etc/settings:
> 
>   init_component "$HOME/.isabelle/contrib/polyml-5.6-1"
> 
> Moreover, it probably requires this adhoc Unix environment variable:
> 
>   export LD_LIBRARY_PATH=$HOME/.isabelle/contrib/polyml-5.6-1/x86-linux
> 
> 
> This is Ubuntu 16.04.5 LTS on Intel(R) Xeon(R) CPU E5-2620 v3 @ 2.40GHz.
> 
> What is actually your system where it happens to work?
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

That's interesting. I suspected one of the "continuous_on" rules would
be the cause. In any case, I don't know how the unification works
exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
apply to this goal at all due to its restrictive type class constraint.

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
machines where it does happen. If this is a race condition, it must be
one of the strangest one I have ever seen (note that it even happens in
single-threaded 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 changeset and now everything is green again (if
>> you excuse the pun).
>>
>> I tracked the problem to a diverging invocation of "blast":
>> https://bitbucket.org/isa-afp/afp-devel/src/e15414dceb2836d07d50546ee94ff8083fbcc80d/thys/Green/Derivs.thy?at=default=file-view-default#Derivs.thy-165
>>
>> However, this "blast" does not diverge on any of my machines, no matter
>> if single-threaded or multi-threaded, no matter if "isabelle build" or
>> Isabelle/jEdit. It actually terminates almost instantaneously.
>>
>> It does, however, seem to diverge reliably on the Testboard, on the
>> workermtahpc, and on isabelle-server. I found this "blast" invocation by
>> running "isabelle jedit" on isabelle-server via XForwarding, and there
>> it was continuously purple and remained purple forever.
> 
> This is indeed a bit strange. Apart from the various AMD machines above,
> I see the same effect on my own Intel Xeon E5-2620 v3.
> 
> 
>> I have no idea why it does that; the proof in question is actually very
>> simple. It does use "continuous_intros" and my changeset does introduce
>> a few new "continuous_intros" rules and also some "intro" rules, but
>> none of them match the goal here at all, so I cannot see how that would
>> influence anything. And I am certainly stumped as to how this kind of
>> non-deterministic behaviour could come about.
> 
> A diff of the two versions of continuous_intros produces the included
> a.patch
> 
> The first rule "continuous_on ?A ?f" is continuous_on_discrete, and
> removing is already sufficient to recover the original proof:
> 
>   supply [continuous_intros del] = continuous_on_discrete
>   by (blast intro!: continuous_intros C1_differentiable_on_pair intro:
> C1_differentiable_on_subset elim: )
> 
> This finishes in 0.250s on my Intel Xeon.
> 
> 
> It would be still nice to understand the problem: maybe something odd
> with higher-order unification, or the unification within blast.
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Manuel Eberl]

Update: I pushed another changeset and now everything is green again (if
you excuse the pun).

I tracked the problem to a diverging invocation of "blast":
https://bitbucket.org/isa-afp/afp-devel/src/e15414dceb2836d07d50546ee94ff8083fbcc80d/thys/Green/Derivs.thy?at=default=file-view-default#Derivs.thy-165

However, this "blast" does not diverge on any of my machines, no matter
if single-threaded or multi-threaded, no matter if "isabelle build" or
Isabelle/jEdit. It actually terminates almost instantaneously.

It does, however, seem to diverge reliably on the Testboard, on the
workermtahpc, and on isabelle-server. I found this "blast" invocation by
running "isabelle jedit" on isabelle-server via XForwarding, and there
it was continuously purple and remained purple forever.

I have no idea why it does that; the proof in question is actually very
simple. It does use "continuous_intros" and my changeset does introduce
a few new "continuous_intros" rules and also some "intro" rules, but
none of them match the goal here at all, so I cannot see how that would
influence anything. And I am certainly stumped as 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 fine locally
> despite trying several times, so I thought it was perhaps some spurious
> issue and pushed the commit anyway.
>
> Unfortunately, "Green" seems to time out on Jenkins every time now.
> Seeing as a while ago, we had spurious timeout issues that went away
> when we increased the timeout, I tried doubling the timeout on the
> Testboard (to 20 minutes!) and that did not help either.
>
> For comparison, on my modest machine, the entry needs a very reasonable
> 2 minutes (both CPU and wall clock) when run with 1 thread, so >20
> minutes seems quite absurd.
>
> I looked at the entry in Isabelle/jEdit and found some invocations of
> blast/force that took up to 8 seconds, but that should not be a problem.
>
> Does anyone have any idea what is going on here or how I could track
> down this issue?
>
> Manuel
>
>
>  Forwarded Message 
> Subject: [Isabelle-ci] Build failure in AFP
> Date: Thu, 30 Aug 2018 22:53:44 +0200 (CEST)
> From: Isabelle/Jenkins 
> To: isabelle...@mail46.informatik.tu-muenchen.de
>
> The AFP build failed. See the log at:
> https://ci.isabelle.systems/jenkins/job/isabelle-all/288/
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2

[Manuel Eberl]

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 are completely unrelated to 
that error and a later test run of virtually the same thing worked fine.

Perhaps this should be investigated before the release.

Manuel


On 2018-07-18 12:53, Makarius wrote:
> This is a reminder that we are in the final consolidation phase towards
> Isabelle2018-RC2.
>
> I will say more precisely when the fork of the isabelle-dev vs.
> isabelle-release repositories will happen, presumably in the next few
> days. After return from FLoC I still need to sort out many details, and
> some genuine problems (apart from inevitable last-minute additions).
>
>
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] quaternions

[Manuel Eberl]

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)
and being reflected. The result is the direction of the reflected ray.

Where it belongs I cannot say; that depends on what kinds of results are
proven about it. I for one would consider this a very ‘applied’ concept
(I know it from ray tracing), so unless we have a concrete application
for it, I'm not sure we need it at all.

Manuel


On 2018-06-18 14:17, Lars Hupel wrote:
>> So where does this material belong? Arguably not in Analysis, which is 
>> already too large.
> Why not a regular AFP entry?
>
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Cannot build HOL (again)

[Manuel Eberl]

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 failing to build, stalling quite 
> reproducibly after about two minutes of processor time. It's a big obstacle 
> to getting any work done, so tips would be welcome.
> 
> Larry
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Algebra

[Manuel Eberl]

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 from École Polytechnique. They have been going over 
> HOL-Algebra and Group-Ring-Module, providing new proofs of the best results 
> in the latter and tidying up some messy proofs in the former, as well. They 
> are also systematising the chaotic naming conventions that they found there. 
> So there will be big changes to HOL-Algebra in the coming weeks. This is an 
> early warning in case anybody else wants to work on this directory.
>
> Larry
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] reflect_poly

[Manuel Eberl]

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 "recip_poly".

Manuel


On 2018-04-16 06:52, Akihisa Yamada wrote:
> Dear HOL-Computational_Algebra developers,
> 
> how about renaming "reflect_poly" in Polynomial.thy to "reciprocal_poly"?
> 
> It seems to be standard to call them "reciprocal polynomials", cf.
> https://en.wikipedia.org/wiki/Reciprocal_polynomial, and the current
> naming wants an extra sentence to relate the notions in paper writing.
> 
> Best regards,
> Akihisa
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

> The test did not finish, although I left it overnight. There is something 
> wrong. I don't know how to identify the problem since the jedit interface 
> seems to work, all files are completely processed.
> 
> I can share may changes with you. I can use "hg serve", unless you know of a 
> better method. The main changes are to HOL, and I updated HOL-Library for 
> these changes.

hg serve is possible. You can also fork the repository on Bitbucket. The
"normal" approach is to just create a Mercurial patch file with "hg
export" or "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...@mailbroy.informatik.tu-muenchen.de> 
> On Behalf Of Manuel Eberl
> Sent: Saturday, March 10, 2018 1:26 AM
> To: isabelle-dev@mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] Complete Distributive Lattice
> 
> 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 non-terminating steps 
> in Isabelle/jEdit?
> 
> If you share your version of HOL-Library with me, I'll happily take a look at 
> it.
> 
> Manuel
> 
> 
> On 09/03/18 23:54, viorel.preote...@gmail.com wrote:
>> I am trying to test HOL-Library by using:
>>
>> ./bin/isabelle build -v HOL-Library
>>
>> But it takes very long. It has now been working for few hours, and it is 
>> still running.
>> I also tried to open all files from HOL/Library in Isabelle/jedit and 
>> they were processed quite fast, without any errors.
>>
>> What is the appropriate way to test HOL-Library?
>>
>> Viorel Preoteasa
>>
>> -Original Message-
>> From: Lawrence Paulson <l...@cam.ac.uk>
>> Sent: Friday, March 9, 2018 12:49 PM
>> To: viorel.preote...@gmail.com
>> Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de
>> Subject: Re: [isabelle-dev] Complete Distributive Lattice
>>
>> I don’t think it’s a problem that your more general theorems require the 
>> Axiom of Choice, and Hilbert_Choice.thy is not too large already (far from 
>> it).
>>
>> Larry Paulson
>>
>>
>>
>>> On 8 Mar 2018, at 21:35, <viorel.preote...@gmail.com> 
>>> <viorel.preote...@gmail.com> wrote:
>>>
>>> I have a question about how to organize these changes. The problem is 
>>> that most of the results for the more general lattice (instantiations 
>>> to set, fun) require Hilbert_Choice which is not available in 
>>> Complete_Lattice. Now I have added all results about complete distributive 
>>> lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this acceptable?
>>>
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabell
>> e-dev
>>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

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 problem.

However, I am still a bit puzzled by the fact that, according to what
you said, everything seems to run through in Isabelle/jEdit. That's not
impossible, but it is somewhat unusual.

Manuel


On 10/03/18 12:46, viorel.preote...@gmail.com wrote:
> I managed to identify this problem. It was one file that did not finish. I 
> made a new session and added the Library files little by little until I found 
> the once causing problems.
> 
> When you build a session, is it possible to find out what file(s) cause 
> problems? If I would know that a certain file takes a certain amount of time, 
> and it does not finish, then I could pin point the problem.
> 
> Viorel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

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 want.

Manuel


On 10/03/18 12:52, viorel.preote...@gmail.com wrote:
> I am trying to build the afp-devel, but the process stops saying "Nothing to 
> build"
> 
> $ ./bin/isabelle build -d ../afp-devel/thys -X slow
> ### Nothing to build
> 0:00:00 elapsed time
> 
> $ ./bin/isabelle build -c -d ../afp-devel/thys -X slow
> ### Nothing to build
> 0:00:01 elapsed time
> 
> Viorel
> 
> -Original Message-
> From: Makarius  
> Sent: Saturday, March 10, 2018 11:29 AM
> To: viorel.preote...@gmail.com; 
> isabelle-dev@mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] Complete Distributive Lattice
> 
> On 09/03/18 23:54, viorel.preote...@gmail.com wrote:
>> I am trying to test HOL-Library by using:
>>
>> ./bin/isabelle build -v HOL-Library
>>
>> But it takes very long. It has now been working for few hours, and it is 
>> still running.
>> I also tried to open all files from HOL/Library in Isabelle/jedit and 
>> they were processed quite fast, without any errors.
> 
> For proposed changes in main HOL, you ultimately need to test all of Isabelle 
> + AFP. This can be quite tiresome, unless you find someone to do it for you.
> 
> The README_REPOSITORY file has more information about testing at the bottom. 
> For AFP you need to include its main session directory like
> this: "isabelle build -d .../AFP/thys -X slow".
> 
> Without "-X slow" you have hardly a chance to finish in reasonable time on 
> normal hardware, but even the "slow" group needs to be tested at some point.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Complete Distributive Lattice

[Manuel Eberl]

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 non-terminating
steps in Isabelle/jEdit?

If you share your version of HOL-Library with me, I'll happily take a
look at it.

Manuel


On 09/03/18 23:54, viorel.preote...@gmail.com wrote:
> I am trying to test HOL-Library by using:
> 
> ./bin/isabelle build -v HOL-Library
> 
> But it takes very long. It has now been working for few hours, and it is 
> still running.
> I also tried to open all files from HOL/Library in Isabelle/jedit and they 
> were processed
> quite fast, without any errors.
> 
> What is the appropriate way to test HOL-Library?
> 
> Viorel Preoteasa
> 
> -Original Message-
> From: Lawrence Paulson  
> Sent: Friday, March 9, 2018 12:49 PM
> To: viorel.preote...@gmail.com
> Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de
> Subject: Re: [isabelle-dev] Complete Distributive Lattice
> 
> I don’t think it’s a problem that your more general theorems require the 
> Axiom of Choice, and Hilbert_Choice.thy is not too large already (far from 
> it).
> 
> Larry Paulson
> 
> 
> 
>> On 8 Mar 2018, at 21:35,  
>>  wrote:
>>
>> I have a question about how to organize these changes. The problem is 
>> that most of the results for the more general lattice (instantiations 
>> to set, fun) require Hilbert_Choice which is not available in 
>> Complete_Lattice. Now I have added all results about complete distributive 
>> lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this acceptable?
>>
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Manuel Eberl]

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 before.

Lipschitz continuity is certainly undergraduate material. That probably
appears in any introductory Analysis lecture, even those for computer
scientists.

Manuel


On 2018-01-19 12:01, Tjark Weber wrote:
> On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote:
>>> One possible criterion: which results 
>>> are part of a standard undergraduate  athematics curriculum?
>> It sounds like a reasonable criterion. Can you tell us what that means for 
>> Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?
> Metric completion features prominently, e.g., in the construction of
> the reals. Lipschitz continuity (along with the Picard–Lindelöf
> theorem) should be part of any course on differential equations.
>
> I can't recall whether I've been taught about Hausdorff distance or
> even isometries during my undergraduate years. Of course, these are
> fairly simple concepts.
>
> Best,
> Tjark
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Manuel Eberl]

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, Lawrence Paulson wrote:
>> This is mainly a negative criterion, i.e., something outside the
>> undergraduate curriculum probably should not be in our core
>> libraries. But I would guess for example mathematicians cover Gödel's
>> theorem, which we would not want to move to our core libraries.
>>
>> Larry
>>
>>> On 18 Jan 2018, at 13:31, Tobias Nipkow  wrote:
>>>
>>> It sounds like a reasonable criterion. Can you tell us what that
>>> means for Hausdorff_Distance, Metric_Completion and Isometries (as
>>> detailed by Fabian)?
>>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

> You could try with a fresh build of Poly/ML:
Okay, I rebuilt Poly/ML (not libsha1 and libgmp though; apparently your
build script does not build those). The crashes still occured though. I
think I did everything correctly, because when I delete the files that
the compilation created, isabelle build fails immediately with some
ML-related error message, so it must have been using them.

> It should be sufficient to remove the is_pure() here:
That does indeed seem to make the problem go away completely. At least I
got about 50 consecutive builds without any crashes now.

Manuel


On 2017-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 Oct 26 13:44:41 2017 +0200
>> summary: use Poly/ML 5.7.1 test version as default;
>> Does Poly/ML 5.7.1 contain any changes that could plausibly cause this
>> bad behaviour to go away?
> One side-condition that has also changed is the build platform: for the
> various Poly/ML 5.6 Isabelle components it was still Ubuntu 10.04 LTS,
> for current Poly/ML 5.7.1 test versions it is Ubuntu 12.04 LTS.
>
> Sometimes there are problems in the C/C++ compiler that disappear over
> time. You could try with a fresh build of Poly/ML: the README in the
> component contains brief instructions how to operate on the included src
> directory.
>
>
>   Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

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
>>> 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 the "-b" has no
>> influence on whether it crashes or not.
> Yes, Pure always produces a heap, independently of the -b option.
>
>
>   Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[Manuel Eberl]

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 locally map it to ML's fixed size "int" instead,
I think.

Manuel


On 2017-11-08 15:36, Tobias Nipkow wrote:
>
>
> On 08/11/2017 14:13, Makarius wrote:
>> On 08/11/17 12:35, Tobias Nipkow wrote:
>>>
>>> On 07/11/2017 23:13, Makarius wrote:
 For Flyspeck-Tame a small performance loss remains. It might be worth
 trying to configure the Isabelle/HOL codegen to use FixedInt
 instead of
 regular (unbounded) Int. Thus it could become faster with Poly/ML
 5.7.1
 than with 5.6.
>>>
>>> Just as for Isabelle itself, I don't want generated code to abort with
>>> overflow or even worse to overflow silently.
>>
>> I also don't want to see FixedInt used routinely instead of proper
>> mathematical Int.
>>
>> The idea above is to provide an option for the HOL codegen that is used
>> specifically for applications like Flyspeck-Tame. It is mainly a
>> question to codegen experts, if that can be done easily.
>
> Then I misunderstood. An optional use of FixedInt for languages where
> overflow raises an exception is fine with me.
>
>> If the answer is "no", I personally don't mind. Flyspeck-Tame runs
>> de-facto only in background builds: 1-2h more or less does not matter so
>> much. Its classic runtime was actually 10h total, now we are at 7h.
>
> In which case I would say that providing such an option should be
> balanced with the complexity it requires or introduces.
>
> Tobias
>
>>
>> Makarius
>>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

> 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 the "-b" has no
influence on whether it crashes or not.

> It's impossible to be sure about any of this without running tests on
> the hardware itself.
I would gladly run any tests that you propose on my hardware. I could
even give you SSH access to a live-CD-like system.

Manuel


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

I was not able to find out what exactly crashes and why, but while
trying to do that, I found out that the problem is actually not present
in the development version of Isabelle anymore.

After a lengthy bisection, I found that the first revision where no
crashes occur is this one:

changeset:   66920:aefaaef29c58
user:    wenzelm
date:    Thu Oct 26 13:44:41 2017 +0200
summary: use Poly/ML 5.7.1 test version as default;

So apparently, something changed in Poly/ML 5.7.1 that made the crashes
go away. Older versions of Isabelle, i.e. Isabelle2016-1, Isabelle2017,
and isabelle-dev up to 66919:1f93e376aeb6 /do/ exhibit the crash. It
thus seems likely that whatever caused it was apparently present in
multiple older Poly/ML versions.

Note that the crash appears to be highly sensitive to the environment:
Having two builds run in parallel with different Isabelle versions seems
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 like this thread is not dead yet.
>
> I had my CPU replaced by a new version that supposedly does not have the
> SMD problem on Linux. The problem with Isabelle did not go away.
>
> I still get reproducible crashes of "isabelle build -c Pure", but only
> with SMT switched on. However, it is worth noting that the crashes
> always seem to happen at the end of the build process. (A successful
> build takes about 9 seconds of elapsed and CPU time on my machine and
> unsuccessful ones always crash at at least that time) However, it is
> worth noting that some of the failed builds look like this:
>
> 0:00:30 elapsed time, 0:00:08 cpu time, factor 0.29
>
> Also, the last line that is printed is always
>
> ### theory "ML_Bootstrap"
>
> so perhaps that also points to some specific problem. However, I don't
> think it's anything specific to Pure, since the crash is also
> reproducible with other sessions if I remember correctly (I just use
> Pure because it can be built quickly).
>
> To summarise:
> - crash happens randomly in about 6% of builds of the "Pure" session
> - crash seems specific to my Ryzen or at least my system
> - disabling SMT makes problem go away
> - crash reproducible on my Arch installation and a fresh install of
> Arch, but not on Ubuntu
> - RAM passes memtest without errors
> - I did not experience instability with any other software
> - My conjecture would be that it is somehow related to PolyML and
> multithreading
>
> I attached both the console output and the build log.
>
> Manuel
>
>
> On 04/09/17 15:12, Manuel Eberl wrote:
>> Alas, it would appear I have spoken too soon!
>>
>> I experienced a strange build failure with RC1 yesterday and, fearing
>> the worst, did my experiment from a few weeks ago again, with the
>> following result:
>>
>> – building "Pure" fails in around 6 % of the cases
>> – this does not change even after a cold reboot
>> – switching SMT off seems to make the problem go away entirely
>> – switching SMT on makes it reappear
>>
>> Sounds very much like this might well be the Ryzen bug. AMD has started
>> replacing affected CPUs, so I shall enquire about that and see what happens.
>>
>> Cheers,
>>
>> Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

Alas, it would appear I have spoken too soon!

I experienced a strange build failure with RC1 yesterday and, fearing
the worst, did my experiment from a few weeks ago again, with the
following result:

– building "Pure" fails in around 6 % of the cases
– this does not change even after a cold reboot
– switching SMT off seems to make the problem go away entirely
– switching SMT on makes it reappear

Sounds very much like this might well be the Ryzen bug. AMD has started
replacing affected CPUs, so I shall enquire about that and see what happens.

Cheers,

Manuel


On 20/08/17 14:31, Manuel Eberl wrote:
> Addendum: I did a system upgrade (including a major kernel upgrade)
> around the same time when I first noticed the problem and I don't think
> I rebooted afterwards, so one very plausible explanation is that Linux
> introduced some workarounds/bug fixes in the 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 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
>> disabled it.
>> – 100 iterations on Ryzen 1800X after a reboot with SMT disabled. No
>> failures.
>> – 100 iterations on Ryzen 1800X after another reboot with SMT enabled
>> again. No failures.
>>
>> So it seems the problem went away as mysteriously as it appeared and it
>> probably has something to do with the hardware or software constellation
>> on my computer. Or perhaps I should check my flat for radiation sources.
>>
>> Cheers,
>>
>> Manuel
>>
>>
>> On 20/08/17 11:24, Lars Hupel wrote:
>>>> Lars, maybe you can run the same test on your machine and see what
>>>> happens there.
>>>
>>> I did, and nothing happened for about 100 iterations. I have a Core
>>> i7-2600. OS is otherwise identical to Manuel (Arch Linux).
>>>
>>>> As for Scala, could a problem in the Scala compiler really lead to the
>>>> JVM segfaulting? I would have thought if the JVM segfaults, that's a bug
>>>> in the JVM. (unless it's a hardware-related issue, of course)
>>>
>>> I've seen it happening, but it is very rare. Still, the coincidence of
>>> crashes during compilation could be explained by random chance (even if
>>> very unlikely). A quick look over Scala's issue tracker reveals no
>>> documented JVM segfaults after 2011.
>>>
>>> Cheers
>>> Lars
>>>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

[Manuel Eberl]

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Manuel Eberl]

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 few months ago. I even wrote on the mailing
list back then, I think. Those definitions should now be equivalent.

I didn't know there was a totient function in HOL-Algebra, otherwise I
would have removed the duplicate back then.

(By the way, I have lots of additional material on the totient function
and related functions that will come to an AFP near you very soon)

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the Isabelle2017 release

[Manuel Eberl]

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 have also the proof that complete linear order is subclass of
> the new complete distributive lattice class.
> 
> Are there any other subclasses of the current complete distributive
> lattice class? This would be something that could cause problems.
> 
> Otherwise, the existing complete distrib lattice is subclass
> of the one that I implemented, so it should not cause any problems.
> All existing results in the current class can be reused without
> modification.
> 
> My theory works now in Isabelle 2016-1, but I can try it in
> Isabelle2017-RC0 also.
> 
> I can try to integrate it, but I don't know how to test it
> to see if there are any problems with something else.
> 
> For reference, I attach the theory file with the new
> class of complete distributive lattice.
> 
> Best regards,
> 
> Viorel
> 
> 
> 
> On 8/24/2017 6:40 PM, Florian Haftmann wrote:
>> As far as I remember, I introduced the complete_distrib_lattice class
>> after realizing the a complete lattice whose binary operations are
>> distributive is not necessarily a distributive complete lattice.  Hence
>> the specification of that type class has been contrieved without
>> consulting literature.
>>
>> Hence that change should be fine if someone is willing to undertake it
>> before the RC stabilization phase.
>>
>> Cheers,
>> Florian
>>
>> Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:
>>> Sounds good to me. Can anybody think of an objection?
>>> Larry
>>>
 On 23 Aug 2017, at 15:17, Viorel Preoteasa > wrote:

 Hello,

 I am not sure if this is the right place to post this message, but
 it is
 related to  the upcoming release as I am prosing adding something
 to the Isabelle library.

 While working with complete distributive lattices, I noticed that
 the Isabelle class complete_distrib_lattice is weaker compared to
 what it seems to be regarded as a complete distributive lattice.

 As I needed the more general concept, I have developed it,
 and if Isabelle community finds it useful to be in the library,
 then I could provide the proofs or integrate it myself in the
 Complete_Lattice.thy

 The only axiom needed for complete distributive lattices is:

 Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈
 Y)})"

 and from this, the equality and its dual can be proved, as well as
 the existing axioms of complete_distrib_lattice and the instantiation
 to bool, set and fun.

 Best regards,

 Viorel


 On 2017-08-21 21:24, Makarius wrote:
> Dear Isabelle contributors,
>
> we are now definitely heading towards the Isabelle2017 release.
>
> The first official release candidate Isabelle2017-RC1 is
> anticipated for
> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
>
> That is also the deadline for any significant additions.
>
>
> I have already updated the important files NEWS, CONTRIBUTORS,
> ANNOUNCE
> in Isabelle/5c0a3f63057d, but it seems that many potential entries are
> still missing.
>
> Please provide entries in NEWS and CONTRIBUTORS for all relevant
> things
> you have done since the last release.
>
>
> Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de 
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

>>>
>>>
>>>
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>>
>>
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

Addendum: I did a system upgrade (including a major kernel upgrade)
around the same time when I first noticed the problem and I don't think
I rebooted afterwards, so one very plausible explanation is that Linux
introduced some workarounds/bug fixes in the 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 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
> disabled it.
> – 100 iterations on Ryzen 1800X after a reboot with SMT disabled. No
> failures.
> – 100 iterations on Ryzen 1800X after another reboot with SMT enabled
> again. No failures.
> 
> So it seems the problem went away as mysteriously as it appeared and it
> probably has something to do with the hardware or software constellation
> on my computer. Or perhaps I should check my flat for radiation sources.
> 
> Cheers,
> 
> Manuel
> 
> 
> On 20/08/17 11:24, Lars Hupel wrote:
>>> Lars, maybe you can run the same test on your machine and see what
>>> happens there.
>>
>> I did, and nothing happened for about 100 iterations. I have a Core
>> i7-2600. OS is otherwise identical to Manuel (Arch Linux).
>>
>>> As for Scala, could a problem in the Scala compiler really lead to the
>>> JVM segfaulting? I would have thought if the JVM segfaults, that's a bug
>>> in the JVM. (unless it's a hardware-related issue, of course)
>>
>> I've seen it happening, but it is very rare. Still, the coincidence of
>> crashes during compilation could be explained by random chance (even if
>> very unlikely). A quick look over Scala's issue tracker reveals no
>> documented JVM segfaults after 2011.
>>
>> Cheers
>> Lars
>>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

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
disabled it.
– 100 iterations on Ryzen 1800X after a reboot with SMT disabled. No
failures.
– 100 iterations on Ryzen 1800X after another reboot with SMT enabled
again. No failures.

So it seems the problem went away as mysteriously as it appeared and it
probably has something to do with the hardware or software constellation
on my computer. Or perhaps I should check my flat for radiation sources.

Cheers,

Manuel


On 20/08/17 11:24, Lars Hupel wrote:
>> Lars, maybe you can run the same test on your machine and see what
>> happens there.
> 
> I did, and nothing happened for about 100 iterations. I have a Core
> i7-2600. OS is otherwise identical to Manuel (Arch Linux).
> 
>> As for Scala, could a problem in the Scala compiler really lead to the
>> JVM segfaulting? I would have thought if the JVM segfaults, that's a bug
>> in the JVM. (unless it's a hardware-related issue, of course)
> 
> I've seen it happening, but it is very rare. Still, the coincidence of
> crashes during compilation could be explained by random chance (even if
> very unlikely). A quick look over Scala's issue tracker reveals no
> documented JVM segfaults after 2011.
> 
> Cheers
> Lars
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

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 -version" to be sure) and the
same thing happened. I got 9 failures in 152 iterations; however, I
never got a JVM segfault with either Scala version; only these "silent
failures". That was on my Ryzen 1800X.

I then did the exact same thing on my laptop (with Scala 2.12.3 though)
and haven't gotten a single failure in over 100 iterations. So maybe
this is the Ryzen bug after all?

Lars, maybe you can run the same test on your machine and see what
happens there.

Manuel


On 19/08/17 21:29, Makarius wrote:
> On 19/08/17 21:27, Makarius wrote:
>> I propose to try the previous Scala release locally, e.g. as follows in
>> $ISABELLE_HOME_USER/etc/settings:
>>
>>   init_component "$HOME/.isabelle/contrib/scala-2.12.2"
> 
> Do not forget "isabelle jedit -b -f" after flipping Scala versions (that
> is not required for changes of the Java version).
> 
> 
>   Makarius
> 
Cleaning Pure ...
Building Pure ...
Pure FAILED
(see also /home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/Pure)
val warning_message: string -> unit
val writeln_message: string -> unit
  end
structure Debugger: DEBUGGER
val it = (): unit
signature NAMED_THEOREMS =
  sig
val add: string -> attribute
val add_thm: string -> thm -> Context.generic -> Context.generic
val check: Proof.context -> string * Position.T -> string
val clear: string -> Context.generic -> Context.generic
val declare: binding -> string -> local_theory -> string * local_theory
val del: string -> attribute
val del_thm: string -> thm -> Context.generic -> Context.generic
val get: Proof.context -> string -> thm list
val member: Proof.context -> string -> thm -> bool
  end
structure Named_Theorems: NAMED_THEOREMS
val it = (): unit
signature JEDIT = sig val check_action: string * Position.T -> string end
structure JEdit: JEDIT
val it = (): unit
Loading theory "Pure"
### theory "Pure"
### 0.436s elapsed time, 0.436s cpu time, 0.016s GC time
Loading theory "ML_Bootstrap"
structure Output_Primitives: OUTPUT_PRIMITIVES
structure Thread_Data: THREAD_DATA
val ML_system_pp = fn: (int -> 'a -> 'b -> PolyML.pretty) -> unit
val it = (): unit
val it = (): unit
structure PolyML:
  sig
structure IntInf:
  sig val gcd: int * int -> int val lcm: int * int -> int end
  end
val it = (): unit
val it = (): unit
### theory "ML_Bootstrap"
### 0.006s elapsed time, 0.006s cpu time, 0.000s GC time
Unfinished session(s): Pure
0:00:32 elapsed time, 0:00:10 cpu time, factor 0.31
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

The Ryzen thing was also on my mind, but I have not experienced any of
those instability issues. From what I read, they are extremely rare
under normal use and the error occured a few seconds after initiating
isabelle build.

Besides, I know that Lars does not have a Ryzen CPU, and it would be a
very strange coincidence that he ran into a different issue that also
leads to a JVM crash.

As for Scala, could a problem in the Scala compiler really lead to the
JVM segfaulting? I would have thought if the JVM segfaults, that's a bug
in the JVM. (unless it's a hardware-related issue, of course)

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 recommend to
>>> enforce a fresh build, e.g. like this:
> 
> The log says "java_command: isabelle.Isabelle_Tool build -b
> HOL-Analysis" so this was really the "isabelle build", after scalac
> compilation was finished.
> 
> Reading the tea leaves further, I see the following potential reasons of
> the crash:
> 
>   * jdk-8u144 (see Isabelle/98afae4308f5)
> 
>   * scala-2.12.3 (see Isabelle/96ad7d5ff613)
> 
>   * hardware: AMD Ryzen 7 1800X Eight-Core Processor
> 
> I've seen occasional press articles discussing problems of AMD Ryzen,
> e.g.
> https://www.phoronix.com/scan.php?page=news_item=Ryzen-Compiler-Issues
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

> 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 ...


Manuel
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x7f25a57c5b6c, pid=13339, tid=0x7f256066c700
#
# JRE version: Java(TM) SE Runtime Environment (8.0_144-b01) (build 1.8.0_144-b01)
# Java VM: Java HotSpot(TM) 64-Bit Server VM (25.144-b01 mixed mode linux-amd64 compressed oops)
# Problematic frame:
# J 2075 C2 scala.util.parsing.combinator.Parsers$Parser$$Lambda$107.apply(Ljava/lang/Object;)Ljava/lang/Object; (16 bytes) @ 0x7f25a57c5b6c [0x7f25a57c5b00+0x6c]
#
# Core dump written. Default location: /home/manuel/hg/afp-devel/core or core.13339
#
# If you would like to submit a bug report, please visit:
#   http://bugreport.java.com/bugreport/crash.jsp
#

---  T H R E A D  ---

Current thread (0x7f25b5e99800):  JavaThread "pool-1-thread-5" daemon [_thread_in_Java, id=13390, stack(0x7f256026c000,0x7f256066d000)]

siginfo: si_signo: 11 (SIGSEGV), si_code: 1 (SEGV_MAPERR), si_addr: 0xf21517da

Registers:
RAX=0x0007c0061210, RBX=0x7f25622e2870, RCX=0xe404fdd3, RDX=0x0007947664a0
RSP=0x7f256066a898, RBP=0xe4000482, RSI=0xf21517ca, RDI=0xf28ece10
R8 =0x0007c01b3230, R9 =0xf1dfb1a3, R10=0xf21517ca, R11=0x0007c01b3230
R12=0x, R13=0x00072027ee98, R14=0xf803c74e, R15=0x7f25b5e99800
RIP=0x7f25a57c5b6c, EFLAGS=0x00010202, CSGSFS=0x002b0033, ERR=0x0004
  TRAPNO=0x000e

Top of Stack: (sp=0x7f256066a898)
0x7f256066a898:   7f25a573cae8 f2152037
0x7f256066a8a8:   7f25a573cae8 e4000482
0x7f256066a8b8:   e4000482 0007f21517d3
0x7f256066a8c8:   000790a8eb00 000794766dd8
0x7f256066a8d8:   7f25a5af59b8 e4000482
0x7f256066a8e8:   7f25a573cae8 000794766e78
0x7f256066a8f8:   000794766e78 e4000482
0x7f256066a908:   7f25a57bd270 0007f2151765
0x7f256066a918:   7f25a5af5b0c 0007c01b1650
0x7f256066a928:   7f25a5b01884 e4000482
0x7f256066a938:   7f25a573cae8 e40de09c
0x7f256066a948:   7f25a573cae8 e4000482
0x7f256066a958:   7f25a57bd270 e40de09c
0x7f256066a968:   7f25a57bd270 000794765550
0x7f256066a978:   7f25a5af5b0c e40d8883
0x7f256066a988:   7f25a57bd270 e40de0a2
0x7f256066a998:   7f25a573cae8 f21519e3
0x7f256066a9a8:   7f25a573cae8 e40de0a2
0x7f256066a9b8:   7f25a57bd270 f21519e3
0x7f256066a9c8:   7f25a5af59b8 f21519e6e40db48e
0x7f256066a9d8:   0007947664a0 f2152177
0x7f256066a9e8:   7f25a5af5a58 f215199f
0x7f256066a9f8:   7f25a573cae8 000794765f60
0x7f256066aa08:   0007c00d41e0 f21519ec
0x7f256066aa18:   7f25a5af5a58 f21519a3947655f0
0x7f256066aa28:   0007947664a0 000794766fa8
0x7f256066aa38:   7f25a5af5a58 f2151e2b6066aa80
0x7f256066aa48:   000794764c40 0007947656f8
0x7f256066aa58:   7f25bc2f28b0 f21519ac
0x7f256066aa68:   7f25a573cae8 7f256066aac0
0x7f256066aa78:   7f25bbcd0e20 f21519ac
0x7f256066aa88:   7f25a5af59b8 f21519afb5e99800 

Instructions: (pc=0x7f25a57c5b6c)
0x7f25a57c5b4c:   5b 30 49 b8 30 32 1b c0 07 00 00 00 4d 3b d8 75
0x7f25a57c5b5c:   30 49 8b f2 48 c1 e6 03 90 48 b8 ff ff ff ff ff
0x7f25a57c5b6c:   ff ff ff e8 14 d9 d7 ff 44 8b 58 08 41 81 fb 27
0x7f25a57c5b7c:   64 03 f8 75 24 48 83 c4 20 5d 85 05 74 14 74 17 

Register to memory mapping:

RAX=0x0007c0061210 is pointing into metadata
RBX={method} {0x7f25622e2870} 'apply' '(Ljava/lang/Object;)Ljava/lang/Object;' in 'scala/util/parsing/combinator/Parsers$Parser$$Lambda$107'
RCX=0xe404fdd3 is an unknown value
RDX=0x0007947664a0 is an oop
scala.util.parsing.input.CharSequenceReader 
 - klass: 'scala/util/parsing/input/CharSequenceReader'
RSP=0x7f256066a898 is pointing into the stack for thread: 0x7f25b5e99800
RBP=0xe4000482 is an unknown value
RSI=0xf21517ca is an unknown value
RDI=0xf28ece10 is an unknown value
R8 =0x0007c01b3230 is pointing into metadata
R9 =0xf1dfb1a3 is an unknown value
R10=0xf21517ca is an unknown value
R11=0x0007c01b3230 is pointing into metadata
R12=0x is an unknown value
R13=0x00072027ee98 is an oop
scala.util.DynamicVariable$$anon$1 
 - klass: 'scala/util/DynamicVariable$$anon$1'
R14=0xf803c74e is an unknown value

[isabelle-dev] [158c513a39f5] JVM crash

[Manuel Eberl]

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 said
"HOL-Computational_Algebra FAILED", but the log did not contain any
error messages. The last message was

### theory "HOL-Computational_Algebra.Polynomial_Factorial"
### 10.690s elapsed time, 39.546s cpu time, 6.455s GC time

I wonder if this could also be due to a JVM crash.

Cheers,

Manuel
### Building Isabelle/Scala ...
Changed files:
  Admin/build_status.scala
  GUI/wrap_panel.scala
  General/file.scala
  General/http.scala
  General/path.scala
  General/url.scala
  PIDE/command.scala
  PIDE/document.scala
  PIDE/document_id.scala
  PIDE/markup.scala
  PIDE/protocol.scala
  PIDE/session.scala
  PIDE/xml.scala
  System/isabelle_tool.scala
  System/system_channel.scala
  Thy/html.scala
  Thy/sessions.scala
  Thy/thy_header.scala
  Tools/imports.scala
  Tools/server.scala
  library.scala
  ../Tools/Graphview/graph_panel.scala
  ../Tools/Graphview/tree_panel.scala
  ../Tools/VSCode/src/build_vscode.scala
  ../Tools/VSCode/src/grammar.scala
  ../Tools/VSCode/src/preview_panel.scala
  ../Tools/VSCode/src/protocol.scala
  ../Tools/VSCode/src/server.scala
  ../Tools/VSCode/src/state_panel.scala
  ../Tools/VSCode/src/vscode_javascript.scala
  ../Tools/VSCode/src/vscode_rendering.scala
  ../Tools/VSCode/src/vscode_resources.scala
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x7f25a57c5b6c, pid=13339, tid=0x7f256066c700
#
# JRE version: Java(TM) SE Runtime Environment (8.0_144-b01) (build 
1.8.0_144-b01)
# Java VM: Java HotSpot(TM) 64-Bit Server VM (25.144-b01 mixed mode linux-amd64 
compressed oops)
# Problematic frame:
# J 2075 C2 
scala.util.parsing.combinator.Parsers$Parser$$Lambda$107.apply(Ljava/lang/Object;)Ljava/lang/Object;
 (16 bytes) @ 0x7f25a57c5b6c [0x7f25a57c5b00+0x6c]
#
# Core dump written. Default location: /home/manuel/hg/afp-devel/core or 
core.13339
#
# An error report file with more information is saved as:
# /home/manuel/hg/afp-devel/hs_err_pid13339.log
#
# If you would like to submit a bug report, please visit:
#   http://bugreport.java.com/bugreport/crash.jsp
#
/home/manuel/hg/isabelle/lib/scripts/getfunctions: line 1: 13339 Aborted
 (core dumped) "$JAVA_HOME/bin/$PRG" "$@"
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release of Isabelle2017

[Manuel Eberl]

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, by ‘printing of "nat" values’ I was only referring to what
you get when you type "value" etc. Now you won't get a screen full of
"Suc" when you do "value (1000 :: nat)", although computing with large
"nat" values is still relatively slow, as it uses "Suc" internally.

I am no expert on code generation, but I would imagine getting rid of
that (e.g. in favour of binary arithmetic, as is done for "int") is
probably non-trivial. What do our code generatione experts say?

In any case, it's probably not very important; "value" without
Code_Target_Numeral is mostly used for small-scale testing and the
current solution works fine for that.

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release of Isabelle2017

[Manuel Eberl]

Nothing fancy, just a couple of code_post rules to rewrite successor
notation into numeral notation after evaluation and before printing. I
don't know if there's a better way to do that, but I think we discussed
this on the mailing list a while ago and came to the conclusion that
code_post is indeed the way to go.

Of course, I am always open to better solutions, perhaps avoiding the
successor notation entirely, but I don't know the code generator well
enough to say if this is possible (or where the successor stuff comes
from in the first place)

In any case, I would argue that even those 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:
>>
>> the proper printing of "nat" values as numerals instead of successor 
>> notation.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release of Isabelle2017

[Manuel Eberl]

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 months after Isabelle2016-1 (December 2016).
> Following the standard schedule, the Isabelle2017 release should appear
> at the start of October 2017.
>
> During the last 3 weeks in July, I will be in Cambridge. That is also a
> possibility to show me old and new problems in my areas of
> responsibility. Afterwards, I want to finish the reform of
> session-qualified theory names, and put Isabelle/VSCode into shape for
> its 1.0  release.
>
>
> Is there anything else to take into account for this late-summer release
> process?
>
> It is important to recall that the deadline for significant changes is
> actually 6 weeks before the final lift-off, i.e. at the point where the
> fork of isabelle-dev and isabelle-release repositories happens.
>
>
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

[Manuel Eberl]

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 what about the suggestion of just writing "strict_mono" instead?
Besides, you can always introduce local abbreviations for things with
"notation" and delete them with "no_notation" afterwards.

> By the way, I recently encountered a similar (and even more nasty)
> name clash, with compact. The following works perfectly

It's "Topological_Spaces.compact" and that should definitely work. We
should probably make the one from Complete_Partial_Order2 qualified. In
my opinion, there is no question that "compact" should be "compact" in
the topological sense.

Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

[Manuel Eberl]

I agree about 90%, I think, but one could argue that "subseq" contains
additional meta-information: the semantic meaning is that it is a
strictly monotonic function, but the idea behind it is that it describes
a sub-sequence of some other sequence.

Still, I for one think this is not really worth the trouble of keeping
an entirely separate constant around, especially because "subseq h" does
not make much sense: "h" itself is not a subsequence of anything, "f ∘
h" is a sub-sequence of "f".

It would be interesting to know what other users of Complex_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 further, it is nothing more than "strict_mono"
>> restricted to "nat ⇒ nat", so one may well argue that it is
>> superfluous anyway.
>
> If we can get rid of it all together, surely that is the best option?
>
> Tobias
>
>> The possibility of renaming one of them to "subsequence" or
>> "is_subseq" is, in my opinion, not a satisfactory solution, since we
>> would then /still/ have two completely different constants with
>> essentially the same name, just with an arbitrary artificial
>> difference. We might as well call one of them subseq'.
>>
>> The advantage of qualified names is that they really allow us to add
>> disambiguating context to ambiguous names when necessary, e.g.
>> something like "List.subseq" and "Topological_Spaces.subseq". Still,
>> as I said, I do understand that typing such lengthy names is tedious.
>>
>> I currently see the following possible solutions:
>>
>> – find another good name for one of the two things currently named
>> "subseq" and rename it
>> – introduce an arbitrary distinction like "subsequence" or "is_subseq"
>> – move "subseq" to List.thy and make it qualified, so that one must
>> write "List.subseq"
>> – remove Topological_Spaces.subseq entirely, replacing it by strict_mono
>> – leave everything as it is
>>
>> Incidentally, I wonder if it is possible to locally prefer one of the
>> two constants, i.e. say that, in the following block, I want "subseq"
>> to mean "Topological_Spaces.subseq". That might also mitigate the
>> problem of long qualified names.
>>
>> Manuel
>>
>>
>>
>> On 2017-06-30 16:23, Tobias Nipkow wrote:
>>> In theory that solves the problem, but the point is that
>>> Topological_Spaces.subseq is impractical for a frequently used
>>> symbol. 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 Eberl <ebe...@in.tum.de
>>>>> <mailto:ebe...@in.tum.de>> wrote:
>>>>>
>>>>> Yes, I noticed that as well. I decided to leave it that way since,
>>>>> well,
>>>>> we do have qualified names.
>>>>
>>>>
>>>>
>>>> ___
>>>> isabelle-dev mailing list
>>>> isabelle-...@in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>>
>>>>
>>>
>>>
>>>
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

[Manuel Eberl]

I do understand that argument, but I am not sure if
Topological_Spaces.subseq is really used /that/ often. Actually, going
one step further, it is nothing more than "strict_mono" restricted to
"nat ⇒ nat", so one may well argue that it is superfluous anyway.

The possibility of renaming one of them to "subsequence" or "is_subseq"
is, in my opinion, not a satisfactory solution, since we would then
/still/ have two completely different constants with essentially the
same name, just with an arbitrary artificial difference. We might as
well call one of them subseq'.

The advantage of qualified names is that they really allow us to add
disambiguating context to ambiguous names when necessary, e.g. something
like "List.subseq" and "Topological_Spaces.subseq". Still, as I said, I
do understand that typing such lengthy names is tedious.

I currently see the following possible solutions:

– find another good name for one of the two things currently named
"subseq" and rename it
– introduce an arbitrary distinction like "subsequence" or "is_subseq"
– move "subseq" to List.thy and make it qualified, so that one must
write "List.subseq"
– remove Topological_Spaces.subseq entirely, replacing it by strict_mono
– leave everything as it is

Incidentally, I wonder if it is possible to locally prefer one of the
two constants, i.e. say that, in the following block, I want "subseq" to
mean "Topological_Spaces.subseq". That might also mitigate the problem
of long qualified names.

Manuel



On 2017-06-30 16:23, Tobias Nipkow wrote:
> In theory that solves the problem, but the point is that
> Topological_Spaces.subseq is impractical for a frequently used symbol.
> 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 Eberl <ebe...@in.tum.de
>>> <mailto:ebe...@in.tum.de>> wrote:
>>>
>>> Yes, I noticed that as well. I decided to leave it that way since,
>>> well,
>>> we do have qualified names.
>>
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Efficient code for Discrete.log

[Manuel Eberl]

Thanks for the hint!

I'll try to use that then. However, the main goal was to use PolyML's
native log2 function anyway, which is likely much faster than anything
we can implement in Isabelle.

Manuel


On 2017-06-29 20:12, Thiemann, Rene wrote:
> Hi Manual,
> 
> thanks for your efforts, but I believe there is already a more efficient way 
> to compute log2.
> 
> In your implementation, consider your intlog2_aux which roughly requires y 
> iterations if log2(x) = y,
> since you always just add 1 to the accumulator.
> 
> For some of my applications this implementation is not efficient enough, 
> which was the reason to develop Sqrt_Babylonian/Log_Impl.thy,
> which is much faster since it only needs log2(y) iterations: 
> in log_main the accumulator is roughly doubled in every iteration.
> 
> To test, try to compute "log_2 (3 ^ n)” for some 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 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 actually reside? I cannot really put it 
>> into Discrete.thy, because then that would have to import 
>> Code_Target_Numeral. I could put it into Code_Target_Integer.thy, but then 
>> that would have to import Discrete, which does not sound right to me either.
>>
>> I attached what I have so far.
>>
>> Manuel
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Efficient code for Discrete.log

[Manuel Eberl]

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 actually reside? I cannot really put
it into Discrete.thy, because then that would have to import
Code_Target_Numeral. I could put it into Code_Target_Integer.thy, but
then that would have to import Discrete, which does not sound right to
me either.

I attached what I have so far.

Manuel

theory Efficient_Log2
imports
  Main
  "~~/src/HOL/Library/Discrete" 
  "~~/src/HOL/Library/Code_Target_Numeral"
begin

context
includes integer.lifting
begin

qualified lift_definition intlog2 :: "integer \ integer" is
  "\n. int (Discrete.log (nat n))" .

qualified function intlog2_aux :: "integer \ integer \ 
integer" where
  "intlog2_aux n acc = (if n < 2 then acc else intlog2_aux (n div 2) (acc + 1))"
  by auto
termination proof (relation "measure (nat_of_integer \ fst)")
  fix n acc :: integer
  assume "\n < 2"
  hence "nat_of_integer (n div 2) < nat_of_integer n"
by transfer auto
  thus "((n div 2, acc + 1), (n, acc)) \ measure (nat_of_integer \ 
fst)" 
by simp
qed simp_all

declare intlog2_aux.simps [simp del]
  
qualified lemma intlog2_aux_correct: "acc \ 0 \ intlog2_aux 
n acc = intlog2 n + acc"
proof (induction n acc arbitrary: acc rule: intlog2_aux.induct)
  case (1 n acc)
  show ?case
  proof (cases "n < 2")
case True
hence "intlog2 n = 0" by transfer (simp add: Discrete.log.simps)
with True show ?thesis by (subst intlog2_aux.simps) auto
  next
case False
hence "intlog2 n = intlog2 (n div 2) + 1"
proof (transfer, goal_cases)
  case (1 m)
  hence "int (Discrete.log (nat m)) = int (Discrete.log (nat m div 2)) + 1"
by (subst Discrete.log.simps) auto
  also have "nat m div 2 = nat (m div 2)" by simp
  finally show ?case .
qed
with False show ?thesis by (subst intlog2_aux.simps) (auto simp: 1)
  qed
qed
  
qualified lemma intlog2_code [code]: "intlog2 n = intlog2_aux n 0"
  by (simp add: intlog2_aux_correct)

lemma Discrete_log_code [code abstract]:
  "integer_of_nat (Discrete.log n) = (if n = 0 then 0 else intlog2 (of_nat n))"
  by transfer simp

end

code_printing
  constant "Efficient_Log2.intlog2 :: integer \ _" 
\ 
(SML) "IntInf.log2" and
(Eval) "IntInf.log2"

value [code] "Discrete.log 12345"

export_code Discrete.log checking SML Eval Scala Haskell? OCaml?

end___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

[Manuel Eberl]

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 development version,
> I've just noticed that the renaming of sublisteq to subseq done by
> Manuel in May (639eb3617a86) has one bad effect:
> 
> The name subseq is already used in Topological_Spaces to formalise the
> concept of a subsequence. This name is now hidden by the definition in
> Sublist, in particular when I import HOL-Probability.
> 
> Can this name clash be eliminated before the next release such that I
> don't have to write Topological_Spaces.subseq everywhere?
> 
> Thanks,
> Andreas
> 
> On 26/05/17 08:16, Tobias Nipkow wrote:
>> Thank you for your research. I am perfectly happy with "sublist" (for
>> the contiguous case) and "subseq" (for the general case) and think we
>> should adopt it.
>>
>> [Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒
>> nat set ⇒ 'a list" (in List) to something else, eg sublist_index)
>>
>> Tobias
>>
>> On 25/05/2017 21:13, Jasmin Blanchette wrote:
>>>
 On 25.05.2017, at 20:41, Tobias Nipkow  wrote:

 I don't think that sublist, subsequence and substring really have
 much of a bias in either direction, except possibly substring, but
 the latter does indeed sound too specialized.
>>>
>>> Wikipedia has a clear bias (and I did not edit it, nor did I look it
>>> up before writing my previous email):
>>>
>>> https://en.wikipedia.org/wiki/Subsequence
>>> https://en.wikipedia.org/wiki/Substring
>>>
>>> Popular algorithm sbooks like Cormen et al. follow the same
>>> definition of subsequence. Standard expressions like "longest
>>> increasing subsequence" depend on this semantics.
>>>
>>> As for sublist, all the examples I see by Googling either "sublist",
>>> "is_sublist", "isSublist", or "indexOfSubList" in Java, Python,
>>> Scala, etc., have the contiguous semantics. Including this page:
>>>
>>> http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html
>>>
>>> I'm not saying we should rename the Isabelle concepts, just that
>>> Isabelle is the odd (wo)man out.
>>>
>>> Jasmin
>>>
>>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build Problem in JinjaThreads

[Manuel Eberl]

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 Haftmann wrote:

isabelle: 3bec939bd808 tip
afp: 09eedef13195 tip


***   {n. enat n < llength stls \
***   (case lnth stls n of
***(s, tl, s') \ \ \move s tl s')} ::
***   nat set
***
*** Coercion Inference:
***
*** Local coercion insertion on the operand failed:
*** Cannot generate coercion from "??'a26 set" to "'a"
***
*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** weak unification of subtype constraints fails
***
***
*** At command "hence" (line 512 of 
"/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")
*** Type unification failed
***
*** Type error in application: incompatible operand type
***
*** Operator:  lsublist tls :: 'a \ 'tl llist
*** Operand:
***   {n. enat n < llength stls \
***   (case lnth stls n of
***(s, tl, s') \ \ \move s tl s')} ::
***   nat set
***
*** Coercion Inference:
***
*** Local coercion insertion on the operand failed:
*** Cannot generate coercion from "??'a26 set" to "'a"
***
*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** weak unification of subtype constraints fails
***
***
*** At command "hence" (line 512 of 
"/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")

Any suggestion what is going on here?

Cheers,
Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

[Manuel Eberl]

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 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.

Excellent, thanks.

Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Sporadic build failure of HOL-Probability in 16a8991ab398

[Manuel Eberl]

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
/home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/HOL-Probability)

(full console output and build log attached).

There is absolutely nothing in the build log that indicates an error to
me. Also, I built HOL-Probability (without -b) a few minutes before that
and it went through fine, and when I built it again a few minutes after
the failure, it also worked fine.

For completeness, the tests were executed on an up-to-date Arch Linux
with 32 GB of RAM and a completely fresh Isabelle installation; i.e. no
settings were modified except that AFP was registered as a component. In
particular, it ran in 32 bit mode.

Cheers,

Manuel
Building Landau_Analysis ...
Finished Landau_Analysis (0:00:29 elapsed time, 0:01:07 cpu time, factor 2.31)
Building HOL-Number_Theory ...
Finished HOL-Number_Theory (0:01:09 elapsed time, 0:03:57 cpu time, factor 3.43)
Building Lehmer ...
Finished Lehmer (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.90)
Building Pratt_Certificate ...
Finished Pratt_Certificate (0:00:25 elapsed time, 0:01:05 cpu time, factor 2.57)
Building HOL-Probability ...
HOL-Probability FAILED
(see also /home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/HOL-Probability)
### ("\<^const>Fun.comp" ("_position" f) ("_position" X))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate rewrite rule:
### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True
### Ignoring duplicate rewrite rule:
### inverse ?a1 \ (1::?'a1) / ?a1
### Ignoring duplicate rewrite rule:
### inverse ?a1 ^ ?n1 \ inverse (?a1 ^ ?n1)
### Ignoring duplicate rewrite rule:
### ((1::?'a1) / ?a1) ^ ?n1 \ (1::?'a1) / ?a1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 / ?b1) ^ ?n1 \ ?a1 ^ ?n1 / ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True
### Ignoring duplicate rewrite rule:
### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True
### Ignoring duplicate rewrite rule:
### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True
### Ignoring duplicate rewrite rule:
### frontier {..?a1} \ {?a1}
### Ambiguous input (line 1868 of "~~/src/HOL/Probability/Information.thy") 
produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
### ("\<^const>local.mutual_information_Pow" ("_position" X)
###   ("_position" Z))
### ("\<^const>Groups.minus_class.minus"
###   ("\<^const>local.entropy_Pow" ("_position" X))
###   ("\<^const>local.entropy_Pow"
### ("\<^const>HOL.disj" ("_position" X) ("_position" Z))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
### ("\<^const>local.mutual_information_Pow" ("_position" X)
###   ("_position" Z))
### ("\<^const>Groups.minus_class.minus"
###   ("\<^const>local.entropy_Pow" ("_position" X))
###   ("\<^const>local.conditional_entropy_Pow" ("_position" X)
### ("_position" Z)
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
Quick_Sort_Cost CANCELLED
Running Bertrands_Postulate ...
^[^EFinished Bertrands_Postulate (0:01:15 elapsed time, 0:02:46 cpu time, 
factor 2.21)
Running Euler_MacLaurin ...
Finished Euler_MacLaurin (0:00:16 elapsed time, 0:00:32 cpu time, factor 1.95)
Random_BSTs CANCELLED
Unfinished session(s): HOL-Probability, Quick_Sort_Cost, Random_BSTs
0:05:30 elapsed time, 0:14:56 cpu time, factor 2.71


Loading theory "HOL-Probability.Fin_Map" (required by "Probability" via 
"HOL-Probability.Projective_Limit")
Loading theory "HOL-Probability.Discrete_Topology" (required by "Probability")
Loading theory "HOL-Probability.Probability_Measure" (required by "Probability" 
via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via 
"HOL-Probability.Characteristic_Functions" via 
"HOL-Probability.Weak_Convergence" via "HOL-Probability.Distribution_Functions")
Loading theory "HOL-Probability.Essential_Supremum" (required by "Probability")
Loading theory "HOL-Probability.Stopping_Time" (required by "Probability")
locale prob_space =
  fixes M :: "'a measure" 
  assumes "prob_space M"
instantiation
  discrete :: (type) metric_space
  dist_discrete == dist ::
'a discrete \ 'a discrete \ real
  uniformity_discrete == uniformity ::
('a discrete \ 'a discrete) filter
  open_discrete == open :: 'a discrete set \ bool
locale filtration =
  fixes \ :: "'a set" 
and F :: "'t \ 'a measure" 
  assumes "filtration \ F"
### theory "HOL-Probability.Discrete_Topology"
### 0.310s elapsed time, 1.793s cpu time, 0.063s GC time
### theory "HOL-Probability.Essential_Supremum"
### 0.315s elapsed time, 1.837s cpu time, 0.063s GC 

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

[Manuel Eberl]

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 code equation breaks Scala code generation in 
>> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Changed theory merge behaviour

[Manuel Eberl]

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 short: apparently, importing a theory (e.g. Library/Multiset) twice
in two theories A and B can be problematic when the theory import is
done in different ways (e.g. once as "~~/src/HOL/Library/Multiset" and
once as "Multiset" by another theory in Library).

This can cause the theory merge to fail when importing both theories A
and B in a third theory C, but I was unable to extract a minimal example
– apparently, it doesn't /always/ happen.

One example of this behaviour in the wild is
Library/Formal_Power_Series, where I think the clash is caused by the
GCD theory. Another is Euler_MacLaurin in the AFP, where the clas is
caused by Multiset.

Strangely enough, this does /not/ happen when using "isabelle build"; it
only happens in Isabelle/jEdit, which is why the CI tests did not catch it.

There was no NEWS entry for this changed behaviour and I am a bit
confused about how to proceed now. Is this discrepancy between build and
IDE intended? Is there some canonical way to write import paths and the
affected theories violate it somehow?

Cheers,

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] SQLite-related error in testboard-afp job

[Manuel Eberl]

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 missing database (no such
table: isabelle_session_info)
17:32:12 Build step 'Execute shell' marked build as failure

Does anybody know anything about this?

Cheers,

Manuel


[1]: https://ci.isabelle.systems/jenkins/job/testboard-afp/336/consoleFull
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The Great Picard Theorem

[Manuel Eberl]

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 wrong about this.

I could perhaps ask around a bit.

I for one am quite open to the idea of moving more material from the
distribution to the AFP, especially from HOL-Analysis. Picard's theorem
sounds like a reasonable candidate for that, but in general, I also have
no idea where to draw the line.

Cheers,

Manuel


On 22/02/17 17:46, Lawrence Paulson wrote:
> I have just added this to the Analysis directory, making its inevitable 
> refactoring more necessary.
> 
> Arguably it should be an AFP entry. Unfortunately, I’m not sufficiently 
> expert in complex analysis to say whether it is core material or not. It 
> looks like a fundamental result to me.
> 
> We should probably resolve the question of Analysis before the next release. 
> How do we decide which things go into Complex_Main versus Analysis (which 
> could be split into basic/advanced) and the AFP?
> 
> Larry
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Old_Number_Theory

[Manuel Eberl]

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 convention and I 
must have missed it. I will take care of it at once.


Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Old_Number_Theory

[Manuel Eberl]

True, but even though I am hardly an expert in number theory, I would 
imagine that a solid foundation in analysis (especially complex 
analysis) is very helpful, if not indispensable, in the development of 
advanced number theory. (the most obvious example is the 
complex-analytic proof of PNT and the Riemann ζ function)


So I think if anyone wants to work on this in the future, I think we 
have a lot of nice building blocks available.


Cheers,

Manuel


On 18/10/16 13:27, Lawrence Paulson wrote:

That is great news!

It’s a pity that our coverage of number theory is minuscule compared 
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 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 do not think the work necessary to achieve that is worth it.


The vast majority of the porting work was done by a student of ours, 
Jaime Mendizabal Roche, so big thanks to him. He even extended the 
‘two squares’ AFP entry a bit, showing the converse direction as well.



Cheers,

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Old_Number_Theory

[Manuel Eberl]

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 do 
not think the work necessary to achieve that is worth it.


The vast majority of the porting work was done by a student of ours, 
Jaime Mendizabal Roche, so big thanks to him. He even extended the ‘two 
squares’ AFP entry a bit, showing the converse direction as well.



Cheers,

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the release

[Manuel Eberl]

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 12/10/16 11:36, Makarius wrote:
> After the public appearance of Isabelle2016-1-RC0 some days ago, we are
> still in consolidation mode for the Isabelle repository -- lets say at
> least 2 more weeks.
> 
> Isabelle2016-1-RC1 will still be based on the isabelle-dev repository,
> to simplify immediate reactions on suggestions and observations by testers.
> 
> The repository fork to isabelle-release will happen after RC1.
> 
> 
> I am presently still stuck updating the Admin area.
> 
> Are there any non-trivial chunks still in the commit/push pipeline that
> need special considerations?
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Of lazy lists and friendly corecs

[Manuel Eberl]

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:


primcorec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
  "lmerge xs ys = (if lnull xs then ys
   else if lnull ys then xs
   else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge 
(ltl xs) ys)

   else LCons (lhd ys) (lmerge xs (ltl ys)))"

I've still not fully understood what ‘friendly’ means, but I should be 
very surprised if this function were not friendly. So I tried this:


friend_of_corec lmerge where
  "lmerge xs ys = (if lnull xs ∧ lnull ys then LNil
   else if lnull xs then LCons (lhd ys) (ltl ys)
   else if lnull ys then LCons (lhd xs) (ltl xs)
   else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge 
(ltl xs) ys)

   else LCons (lhd ys) (lmerge xs (ltl ys)))"

Unfortunately, I get the following error:

exception TYPE raised (line 168 of "consts.ML"): Illegal type for 
constant "Coinductive_List.llist.LNil" :: 'b


I now have the following questions:
1. Something like "if lnull xs then ys" works in primcorec, but in corec 
and friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl 
ys)". Is that a known limitation?
2. What is the relationship between primcorec and friendliness? If I 
have a function defined by primcorec, is the additional step with 
friend_of_corec fundamentally necessary or is that just a technical 
issue? (I would have naïvely assumed that primitively-corecursive 
functions are always friendly or something like that)

3. What causes the above error and how do I get around it?


Cheers,

Manuel


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fisher–Yates in AFP

[Manuel Eberl]

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!

Manuel


On 04/10/16 13:16, Lars Hupel wrote:

It isn’t only about SourceTree. As I mentioned, manually adding Fisher_Yates had no 
effect, and even now "hg diff” shows nothing, even though Fisher_Yates should 
appear as “added” or untracked (given that it’s on my machine and nowhere else). 
I’ve also checked every .hgignore file.

Possibly my copy of the AFP has got corrupted somehow.

I just checked the submission Manuel uploaded to the submission system
and there seems to be an extra ".hg" folder in there. So possibly
Mercurial ignores that directory. It might get fixed by "rm -rf"ing that
extra folder.

Cheers
Lars


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fisher–Yates in AFP

[Manuel Eberl]

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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

[Manuel Eberl]

Hm, that sounds reasonable.

However, I am not sure whether using "finite" is really such a good
idea; it will lead to people having to instantiate "finite_UNIV" for all
kinds of things all the time.

I think I once considered a similar solution using a copy of "finite"
that does Code.abort in cases where finiteness wasn't obvious (e.g.
complement), but I abandoned that idea for some reason. Still, at the
moment, I think that might be the best solution.

Any thoughts?

Manuel


On 03/10/16 17:37, Andreas Lochbihler wrote:
> Hi Manuel,
> 
> Indeed, generic iteration over a set is only well-defined if the set is
> finite. For an infinite set, the generic iteration combinator returns an
> unspecified value, not 0 or 1. In fact, I had imagined a code equation
> like you described, namely
> 
>   "Gcd A = (if finite A then ... else Code.abort (Gcd A))"
> 
> Note that this does *not* pull in finite_UNIV. We could implement the
> finiteness test by
> 
>   "finite (set xs) = True"
>   "finite (List.coset ys) = Code.abort (STR ''Finiteness test on
> Complement'') ..."
> 
> If one imports HOL/Library/Card_UNIV or Containers, then one has to
> provide instances for finite_UNIV and a bunch of other type classes
> anyways. That's the price of using more complicated libraries.
> 
> AFAICS, it does not really matter whether the iteration combinator takes
> an additional argument, because they can be expressed in terms of each
> other:
> 
>   fold_default dflt f A x = (if finite A then dflst A else
> Finite_Set.fold f A x)
>   Finite_Set.fold f A x = fold_default (%A. THE ... A ...) f A x
> 
> The advantage of fold_default with a default 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/10/16 16:27, Manuel Eberl wrote:
>> I'm afraid it's not quite as easy as that. You cannot use the existing
>> combinators for comp_fun_commute for Gcd. For infinite sets, these
>> combinators return the neutral element (i.e. "0" for Gcd and "1" for
>> Lcm), but not every infinite set has Gcd 0 or Lcm 1. For setsum/setprod,
>> this works because it is quite simply defined that way, but for Gcd/Lcm
>> it is not.
>>
>> So the alternative would be something like "Gcd A = (if finite A then
>>  else Code.abort …)". This does not work well either,
>> because it requires being able to decide "finite A", which typically
>> introduces the unwanted typeclass requirement "finite_UNIV".
>>
>> My suggestion would be a combinator that, in order to implement a
>> function f :: 'a set => 'a, takes as arguments both a fold operation of
>> type "'a cfc" /and/ the function f itself.
>>
>> It then performs the fold on any "finite by construction" set (e.g. sets
>> represented by the "set" constructor) and returns "Code.abort … (f A)"
>> for anything else (e.g. a set represented by the "coset" constructor).
>>
>> I planned on implementing this at some point, but I've quite a bit of
>> other stuff to do and I wanted to discuss it first, so I never really
>> got around to doing it.
>>
>> Cheers,
>>
>> Manuel
>>
>>
>> On 03/10/16 16:15, Andreas Lochbihler wrote:
>>> Hi René and Manuel,
>>>
>>> Indeed, for sets, expressing the code equations in terms of a generic
>>> iteration operation on sets would do the job for most of the cases. The
>>> comp_fun_commute and comp_fun_idem types  in Containers precisely do
>>> this, but they have not been integrated in the HOL library yet. They
>>> should work all kinds of big operators (setsum, setprod, Gcd, etc) and
>>> could be added to the HOL library.
>>>
>>> Of course, some special case tricks no longer work if go for a generic
>>> iteration operation. For example, one could prove "Gcd (List.coset xs) =
>>> 1" for natural numbers and declare a code equation. Such things would no
>>> longer be possible, but I am not sure whether they 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, Manuel Eberl wrote:
>>>&

Re: [isabelle-dev] Jenkins maintenance

[Manuel Eberl]

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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Manuel Eberl]

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
happen, and that's what Lars did – much of it, as I gather, in his free
time. I'm sure Lars does not object to others adapting this
infrastructure, and he has in fact already implemented a number of
suggestions for improvements.

>From what I have picked up, the new testing infrastructure we have now
is also a lot more adaptable and maintainable than anything we had
before. The words ‘industry standard’ may seem meaningless to you,
Makarius, but it cannot be denied that if /everyone/ does testing in a
certain way these days, then that is at least some evidence that it
might be a good idea to consider. Relying on the vague idea that things
never break because people never make mistakes does not seem like a
sensible approach to me – and once you accept that things /can/ break
because people /do/ make mistakes, prompt notification of /what/ broke
and /why/ is important.

No one is saying that the current state of affairs is optimal. I can
think of a number of possible improvements myself and have privately
communicated them to Lars, who seemed quite grateful for the feedback.

I for one think that a big improvement would be a system where no one
pushes to the repository directly: every push goes to a testing server,
and if the test is successful, the changes can then automatically be
merged into the repository without an additional test. This avoids the
current duplication of tests where one first pushes to the testboard,
waits for everything to run through, and then pushes to the repository
where everything is tested again. It would also be an effective
safeguard against breaking the repository (and possibly even the AFP),
which /does/ happen quite frequently. (cf. the current situation where
things have been broken for days) Another improvement I can think of is
that it would be good to have a little more control over testing:
aborting tests when they are not necessary anymore, testing only the
repository (and not the AFP) etc. All of this we can talk about and find
a solution in time.

It is important here to stress that none of us is working /against/
another – we all want the best possible infrastructure to do our work,
and I for one do not like the path this discussion has been taking. The
reality of it all is that our testing infrastructure was in shambles for
quite some time. Then Lars came along and put in a lot of effort to get
things up and running again. The main response on this mailing list were
vague insinuations that he does not understand how to do tests, or does
not care about doing it properly, which could hardly be farther removed
from the truth.

This email is getting a bit longer than I had planned, so let me
summarise my points once more for additional clarity:
– The current testing infrastructure is good, but not perfect, and we
should work together to make it better.
– The testboard, while also not perfect, has already become an
invaluable tool in my work on both Isabelle and the AFP.
– The tone of the discussion on this mailing list could occasionally do
with a little less passive-aggressiveness and fewer underhanded
insinuations.
– Lars deserves enormous gratitude from all of us for the work he put
into this so far. Of course, this does not mean that his decisions must
not be criticised, but when you work on something (mostly) alone in your
free time and the only public response you get is complaints, that's not
exactly uplifting.


Cheers and a happy Unification Day to all of you,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

[Manuel Eberl]

I'm afraid it's not quite as easy as that. You cannot use the existing
combinators for comp_fun_commute for Gcd. For infinite sets, these
combinators return the neutral element (i.e. "0" for Gcd and "1" for
Lcm), but not every infinite set has Gcd 0 or Lcm 1. For setsum/setprod,
this works because it is quite simply defined that way, but for Gcd/Lcm
it is not.

So the alternative would be something like "Gcd A = (if finite A then
 else Code.abort …)". This does not work well either,
because it requires being able to decide "finite A", which typically
introduces the unwanted typeclass requirement "finite_UNIV".

My suggestion would be a combinator that, in order to implement a
function f :: 'a set => 'a, takes as arguments both a fold operation of
type "'a cfc" /and/ the function f itself.

It then performs the fold on any "finite by construction" set (e.g. sets
represented by the "set" constructor) and returns "Code.abort … (f A)"
for anything else (e.g. a set represented by the "coset" constructor).

I planned on implementing this at some point, but I've quite a bit of
other stuff to do and I wanted to discuss it first, so I never really
got around to doing it.

Cheers,

Manuel


On 03/10/16 16:15, Andreas Lochbihler wrote:
> Hi René and Manuel,
> 
> Indeed, for sets, expressing the code equations in terms of a generic
> iteration operation on sets would do the job for most of the cases. The
> comp_fun_commute and comp_fun_idem types  in Containers precisely do
> this, but they have not been integrated in the HOL library yet. They
> should work all kinds of big operators (setsum, setprod, Gcd, etc) and
> could be added to the HOL library.
> 
> Of course, some special case tricks no longer work if go for a generic
> iteration operation. For example, one could prove "Gcd (List.coset xs) =
> 1" for natural numbers and declare a code equation. Such things would no
> longer be possible, but I am not sure whether they 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, Manuel Eberl wrote:
>> 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 operations from A depend
>> on the implementation that is chosen for sets. A cannot give code
>> equations for every possible implementation of sets, while B cannot
>> possibly import every theory that has operations involving sets and give
>> code equations for it.
>>
>> The best possible solution would be to imitate the way it is currently
>> done for setsum, setprod, etc: Define a sufficiently general combinator
>> that iterates over the set and give the code equations in A in terms of
>> this combinator. Then B only has to reimplement this generic combinator.
>>
>> That would be the cleanest solution, but I'm not sure how such a
>> combinator would look like. The folding operation would probably have to
>> satisfy some associativity/commutativity laws and have that information
>> available at the type level (similar to the cfc type in Containers).
>>
>>
>> By the way, my current workaround for this problem is to declare all
>> problematic constants as "code_abort".
>>
>>
>> Cheers,
>>
>> Manuel
>>
>>
>> On 03/10/16 15:21, Thiemann, Rene wrote:
>>> Dear all,
>>>
>>> in the following theory, the export-code fails:
>>>
>>> (Isabelle 957ba35d1338, AFP 618f04bf906f)
>>>
>>> theory Problem
>>>   imports
>>>   "~~/src/HOL/Library/Polynomial_Factorial"
>>>   "$AFP/thys/Containers/Set_Impl"
>>> begin
>>>
>>> definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
>>>   "foo x y = gcd y x"
>>>
>>> definition bar :: "int ⇒ int" where
>>>   "bar x = foo x (x - 1)"
>>>
>>> export_code bar in Haskell
>>> end
>>>
>>>
>>> The problem arises from two issues:
>>> - factorial_semiring_gcd requires code for
>>>   Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a =>
>>> ‘a”!
>>> - the code-equation for Gcd is Gcd_

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

[Manuel Eberl]

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 operations from A depend
on the implementation that is chosen for sets. A cannot give code
equations for every possible implementation of sets, while B cannot
possibly import every theory that has operations involving sets and give
code equations for it.

The best possible solution would be to imitate the way it is currently
done for setsum, setprod, etc: Define a sufficiently general combinator
that iterates over the set and give the code equations in A in terms of
this combinator. Then B only has to reimplement this generic combinator.

That would be the cleanest solution, but I'm not sure how such a
combinator would look like. The folding operation would probably have to
satisfy some associativity/commutativity laws and have that information
available at the type level (similar to the cfc type in Containers).


By the way, my current workaround for this problem is to declare all
problematic constants as "code_abort".


Cheers,

Manuel


On 03/10/16 15:21, Thiemann, Rene wrote:
> Dear all,
> 
> in the following theory, the export-code fails:
> 
> (Isabelle 957ba35d1338, AFP 618f04bf906f)
> 
> theory Problem
>   imports 
>   "~~/src/HOL/Library/Polynomial_Factorial"
>   "$AFP/thys/Containers/Set_Impl"
> begin
> 
> definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
>   "foo x y = gcd y x" 
>   
> definition bar :: "int ⇒ int" where
>   "bar x = foo x (x - 1)" 
>   
> export_code bar in Haskell 
> end
> 
> 
> The problem arises from two issues:
> - factorial_semiring_gcd requires code for 
>   Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a => ‘a”!
> - the code-equation for Gcd is Gcd_eucl_set: "Gcd_eucl (set xs) = foldl 
> gcd_eucl 0 xs”
>   where “set” is only a constructor if one does not load the 
> container-library.
> 
> It would be nice, if one can either alter factorial_semiring_gcd so that it 
> does not
> require “Gcd” anymore, or if the code-equation is modified in a way that 
> permits
> co-existence with containers. (Of course, similarly for Lcm).
> 
> 
> With best regards,
> Akihisa, Sebastiaan, and René
> 
> PS: We currently solve the problem by disabling Gcd and Lcm as follows:
> 
> lemma [code]: "(Gcd_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Gcd on 
> sets'') (λ _. Gcd_eucl)"  by simp
> lemma [code]: "(Lcm_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Lcm on 
> sets'') (λ _. Lcm_eucl)"  by simp
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Manuel Eberl]

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 one: ∄!

I would vote to forbid the multiple variable case. At least for the
next release. Is it possible to restrict this by a mixfix syntax or
does it require to write a ML parse translations.

  - Johannes

Am Dienstag, den 13.09.2016, 10:30 +0200 schrieb Tobias Nipkow:

There is a method to this madness: if B is a binder, "B x y. t" is
short for "B
x. B y. t". However, I agree that for ∄ and ∃! this is confusing and
one of the
solutions proposed should be adopted.

Tobias

On 13/09/2016 09:45, Peter Lammich wrote:

On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:

We have a problem with the ∄ operator, when existential
quantifiers
are nested:

lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
   by (rule refl)

I do not see a particular problem with this, however, not-exists
and
also exists-one have funny semantics when used with multiple
variables:

lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
 by (rule refl)

lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
 by (rule refl)

this leads to funny lemmas like:

lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
   by presburger

lemma also_strange: "∃!x y. x = abs (y::int)"
   by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
equal_neg_zero)


I would have expected:
(∄x y. P x y) ⟷ ¬(∃x y. P x y)
and
(∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))



We should either forbid multiple variables on those quantifiers, or
try
to figure out whether there is a widely-accepted consensus on their
meaning.

--
   Peter




Note that ∄x y. P x y would be fine.

Larry

~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
abel
le-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
elle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
le-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Manuel Eberl]

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 lately, usually sporadically 
and irreproducibly.


Perhaps the times when 32 Bit Isabelle was enough for all applications 
are indeed over.



Cheers,

Manuel


On 08/08/16 13:06, Makarius wrote:

On 08/08/16 11:14, Lars Hupel wrote:

the latest build failure for the repository is spurious:

*** exception Fail raised (line 83 of "./basis/PolyMLException.sml"):
Insufficient memory

This happened in HOL-Proofs.

I have tried Isabelle/1e7c5bbea36d once again with

   ML_PLATFORM="x86-linux"
   ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.6-1/x86-linux"
   ML_SYSTEM="polyml-5.6"
   ML_OPTIONS="-H 1000 --gcthreads 2"

The result is:

Finished HOL-Proofs (0:17:18 elapsed time, 0:33:38 cpu time, factor 1.94)


Is the test hardware in an air-conditioned server room? Otherwise we
might be actually testing the surrounding temperature or some other
environmental effects.



Makarius, it may or may not be connected to
the recent changes you did in proof reconstruction (994d1a1105ef).

This is merely for printing, which normally does not happen at all.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Primes

[Manuel Eberl]

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", a "prime_factorization"
function, the "factorial_ring" typeclass with instance proofs for
nat, int, poly.

* Probability: Code generation and QuickCheck for Probability Mass
Functions.



As for the former: There are now three new algebraic predicates:

- "irreducible", i.e. irreducible elements in a ring (cannot be
decomposed into
two non-unit factors)
- "is_prime_elem", i.e. p is a prime element if for all x,y where p
divides x *
y, it also divides x or y
- "is_prime" if p is a prime element and it is normalised

For instance, the integer "-3" is a prime element, but not a prime. This
corresponds nicely to the concept of a "prime number" on the integers.
W.r.t.
the old definitions.

The "is_prime" predicate is necessary because normalisation is
necessary for
some things, such as a unique prime factorisation.

The old "prime" constant is now a mere abbreviation for "is_prime" and
can
perhaps be discontinued in the next version. This is not necessarily
the final
naming scheme; I am open to better suggestions.


As a side note, there is a lot of material in this that subsumes
material in
some AFP entries, most notably the "Algebraic Numbers" group by
Thiemann et al.


Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multiset insert

[Manuel Eberl]

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 reason for this, 
I suggest we change it.



On 28/07/16 10:45, Florian Haftmann wrote:

However this is maybe now all too depp-rooted to consolidate it.  Even
if not, alternatives have been proposed here that would resolve that
issue than.


‘depp-rooted’ is now my new favourite word. :D


Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[Manuel Eberl]

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 p" "x ≠ 0" "y ≠ 0"
  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"


Cheers,

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[Manuel Eberl]

As far as I know, ‘multiplicity’ in mathematics is only defined for 
prime factors. That is a luxury that we do not have in HOL, so the 
question is: How do we extend the definition to the full domain?


The obvious possibility would be to just let all non-prime numbers have 
multiplicity 0. This makes a few things look nicer (e.g. the prime 
factors are then precisely the numbers with non-zero multiplicity). 
However, it also means that the multiplicity of "X - 1" in "X² - 1" is 
1, whereas the multiplicity of "1 - X" is 0, which I find a bit odd.


A more general possibility is that which I chose, i.e. the biggest n 
such that p^n divides x. This is well-defined as long as x is non-zero 
and p is not a unit. I would argue that having a more general notion 
like this is nicer.



Cheers,

Manuel


On 19/07/16 12:18, Tobias Nipkow wrote:

Are you 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 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 an integer. The
multiplicity of a non-prime was defined to be 0.

I have now created an alternative definition of "multiplicity" which
is simply
defined as "the highest power that is still a divisor" (as long as
this is
well-defined); e.g. the multiplicity of -4 in 64 would be 3.

I see three possibilities:
1. redefine my "new", more general multiplicity to the "old" multiplicity
2. keep both notions of multiplicity around with different names
3. replace the old multilicity with the new one and adapt all lemmas
accordingly

Currently, I tend towards the last options. Are there any other
opinions on this?


Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] multiplicity and prime numbers

[Manuel Eberl]

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 an integer. The multiplicity of a non-prime was 
defined to be 0.


I have now created an alternative definition of "multiplicity" which is 
simply defined as "the highest power that is still a divisor" (as long 
as this is well-defined); e.g. the multiplicity of -4 in 64 would be 3.


I see three possibilities:
1. redefine my "new", more general multiplicity to the "old" multiplicity
2. keep both notions of multiplicity around with different names
3. replace the old multilicity with the new one and adapt all lemmas 
accordingly


Currently, I tend towards the last options. Are there any other opinions 
on this?



Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Broken AFP

[Manuel Eberl]

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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Scala implicits

[Manuel Eberl]

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 Eberl wrote:

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 
distribution.


I'm glad to see this (hopefully) resolved.


Cheers,

Manuel


On 23/06/16 09:45, Florian Haftmann wrote:

Dear power users of code generation to Scala,

during the last months there have been some reports on ambiguity
problems with implicits in Scala.

One kind of these has been known for long and can be addressed in more
recent versions of Scala, which has been done in 7cffe366d333.

One other kind is presumably resolved with the patch attached,
applicable to b3e5bdb784f5. The key idea is to generate implicits in
Scala (stemming from type class instances) into the respective 
companion

objects of corresponding type classes.

Since I have no example at hand where such ambiguities have been
observed to happen, I would kindly ask whether someone might try 
whether

that patch resolves the issue. No problems on the visible theory
universe (Isabelle distribution plus AFP) have been encountered.

The patch still keeps the traditional Scala approach that each implicit
dictionary holds all operations of all super classes. I don't know
whether this is still apt to expose problems, but this could be tackled
in a second step.

Thanks to Lars Hupel for suggesting these solutions.

Cheers,
Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 






___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Scala implicits

[Manuel Eberl]

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 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 distribution.

I'm glad to see this (hopefully) resolved.


Cheers,

Manuel


On 23/06/16 09:45, Florian Haftmann wrote:

Dear power users of code generation to Scala,

during the last months there have been some reports on ambiguity
problems with implicits in Scala.

One kind of these has been known for long and can be addressed in more
recent versions of Scala, which has been done in 7cffe366d333.

One other kind is presumably resolved with the patch attached,
applicable to b3e5bdb784f5. The key idea is to generate implicits in
Scala (stemming from type class instances) into the respective companion
objects of corresponding type classes.

Since I have no example at hand where such ambiguities have been
observed to happen, I would kindly ask whether someone might try whether
that patch resolves the issue. No problems on the visible theory
universe (Isabelle distribution plus AFP) have been encountered.

The patch still keeps the traditional Scala approach that each implicit
dictionary holds all operations of all super classes. I don't know
whether this is still apt to expose problems, but this could be tackled
in a second step.

Thanks to Lars Hupel for suggesting these solutions.

Cheers,
Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP config files?

[Manuel Eberl]

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

./thys/Catalan_Numbers/config

All the others I gone.

I suspect this is an accidental left-over.

Cheers,
Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Scala implicits

[Manuel Eberl]

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 distribution.


I'm glad to see this (hopefully) resolved.


Cheers,

Manuel


On 23/06/16 09:45, Florian Haftmann wrote:

Dear power users of code generation to Scala,

during the last months there have been some reports on ambiguity
problems with implicits in Scala.

One kind of these has been known for long and can be addressed in more
recent versions of Scala, which has been done in 7cffe366d333.

One other kind is presumably resolved with the patch attached,
applicable to b3e5bdb784f5. The key idea is to generate implicits in
Scala (stemming from type class instances) into the respective companion
objects of corresponding type classes.

Since I have no example at hand where such ambiguities have been
observed to happen, I would kindly ask whether someone might try whether
that patch resolves the issue. No problems on the visible theory
universe (Isabelle distribution plus AFP) have been encountered.

The patch still keeps the traditional Scala approach that each implicit
dictionary holds all operations of all super classes. I don't know
whether this is still apt to expose problems, but this could be tackled
in a second step.

Thanks to Lars Hupel for suggesting these solutions.

Cheers,
Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Manuel Eberl]

Sure, I can do that later today.

By the way, "isabelle build -o document=pdf HOL-Multivariate_Analysis" 
builds the session with document processing enabled. If it fails, it 
tells you both the location of the document directory (with all the 
generated LaTeX files) and the build log.


In my experience, the build log is often too long for me to find the 
errors in it, so I usually just go to the document directory, run 
"pdflatex root.tex" and see where it gets stuck.


Cheers,

Manuel



On 16/06/16 00:13, Lawrence Paulson wrote:

Many thanks for getting to the bottom 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" 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 instances in Brouwer_Fixpoint.thy where you wrote something like 
"R^n" in text, causing the same error.

Cheers,

Manuel



On 15/06/16 18:19, Lawrence Paulson wrote:
No idea what’s going on here. I did commit a lot of stuff but it works on my 
machine. I added a theory, but the addition was committed and I have no 
untracked files. If anybody can figure out what’s going on I'd be grateful. I 
see it is a document preparation failure, presumably that isn’t being checked 
locally for some reason?

Larry


Begin forwarded message:

From: Isabelle/Jenkins <ci@isabelle.systems>
Subject: [Isabelle-ci] Build failure in Isabelle
Date: 15 June 2016 at 17:14:27 BST
To: isabelle...@mail46.informatik.tu-muenchen.de

The Isabelle build failed. See the log at: 
https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/



___
Isabelle-ci mailing list
isabelle...@mail46.informatik.tu-muenchen.de
https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Manuel Eberl]

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 instances in Brouwer_Fixpoint.thy where you wrote 
something like "R^n" in text, causing the same error.


Cheers,

Manuel


On 15/06/16 18:19, Lawrence Paulson wrote:

No idea what’s going on here. I did commit a lot of stuff but it works on my 
machine. I added a theory, but the addition was committed and I have no 
untracked files. If anybody can figure out what’s going on I'd be grateful. I 
see it is a document preparation failure, presumably that isn’t being checked 
locally for some reason?

Larry


Begin forwarded message:

From: Isabelle/Jenkins 
Subject: [Isabelle-ci] Build failure in Isabelle
Date: 15 June 2016 at 17:14:27 BST
To: isabelle...@mail46.informatik.tu-muenchen.de

The Isabelle build failed. See the log at: 
https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/



___
Isabelle-ci mailing list
isabelle...@mail46.informatik.tu-muenchen.de
https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Proper sign of gcd / lcm on type int

[Manuel Eberl]

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. divisibility, where inf = gcd, sup = lcm, Inf = Gcd, Sup 
= Lcm, bot = 1, top = 0.


However, juggling equivalence classes is inconvenient; it is much nicer 
to use representatives, and ideally canonical representatives. This is 
why, in Isabelle, we require that the gcd/lcm be normalised. For natural 
numbers, everything is normalised; for integers, this means that the 
integer is non-negative; for polynomials, it means that the leading 
coefficient is normalised (if the coefficient ring is a field, this 
means the polynomial is zero or must have leading coefficient 1).


I do think that we should enforce the same thing in the ML 
implementation of gcd/lcm. Any definition of gcd/lcm for integers where 
either of them may be negative does not make much sense to me. My guess 
would be that lcm can be negative in the implementation you mentioned 
because the author defined "lcm a b = a * b / gcd a b" with the unstated 
assumption that it is only called for non-negative numbers. Or perhaps 
they thought the sign does not matter.



By the way, speaking of GCDs here and of rational numbers in the other 
thread: I am currently working on a theory of normalised fractions for 
arbitrary GCD rings. This builds on top of Amine Chaiebs fraction 
fields, but additionally requires that the numerator and denominator be 
normalised and the denominator be normalised, which makes the 
representation unique and therefore more convenient.


This theory will then easily be instantiable for polynomials and formal 
power series, yielding rational functions and Laurent series, 
respectively. One could even base Isabelle's rational number theory on 
this more general development in the future.



Cheers,

Manuel



On 31/05/16 21:37, Makarius wrote:

Dear integer experts,

presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to
understand the situation of gcd / lcm for negative arguments.

We have the following slightly divergent operations:

  * HOL gcd / lcm: always >= 0 (via "normalize" which is "abs")

  * PolyML.IntInf.gcd: always >= 0
PolyML.IntInf.lcm: mixed signs, according to product of arguments

  * Integer.gcd / lcm: mixed signs -- IIRC the implementation was only
meant to operate on "nat", which happens to be spelled "int" in ML.

My impression is that the HOL definitions are canonical: several number
theory experts have gone over it over the years. Is this correct?


An investigation of the (very few) uses of the above Poly/ML and
Isabelle/ML operations in Isabelle + AFP supports the following working
hypothesis:

Integer.gcd / lcm should follow the HOL versions, in "normalizing" the
sign, i.e. removing it. (The updated implementation will use
PolyML.IntInf gcd for improved performance.)


Does this sound like a good idea?


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Rat in Isabelle/ML

[Manuel Eberl]

Very good! This is very convenient.




On 01/06/16 21:42, Makarius wrote:

*** ML ***

* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing. Standard operations on type Rat.rat are provided via ad-hoc
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
superseded by General.Div.


This refers to Isabelle/c7de5b311909, which also contains the updated
documentation.

The antiquotation syntax @int/nat for @{Pure.rat argument} is stretching
the existing syntax very little, see 921a5be54132. Further changesets in
the vicinity clean up rat.ML is various repects -- it is surprising how
many details can be missing in such a small module.

I have 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? Anything missing?


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle repository broken

[Manuel Eberl]

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.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle repository broken

[Manuel Eberl]

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:

On 24.05.2016, at 17:12, Makarius  wrote:

The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
6a17bcddd6c2 (eberlm).

The failure is as follows:
### theory "Generate_Binary_Nat"
### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
*** "List.coset" is not a constructor, on left hand side of equation, in
theorem:
*** permutations_of_set (List.coset ?xs) \
...

Looking at the history, it's hard to believe the culprit would be anything but 
change dd651e3f7413.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Factorial ring

[Manuel Eberl]

I agree in principle, but putting up a hierarchy of algebraic structures 
within the constraints of Isabelle's type class system is tricky. 
Additionally, sometimes adjustments have to be made since some things 
that are natural in ‘regular’ mathematics are awkward to express in a 
theorem prover.


For instance, Florian explained to me that working with an equivalence 
relation like associatedness (i.e. two elements divide each other) is 
tedious in Isabelle, whereas working with equations is easy. Therefore, 
introducing a "normalisation" operation that essentially picks one 
distinguished representative from that equivalence class (e.g. the 
non-negative one in case of integers, the monic one in case of 
polynomials) and expressing associatedness as "normalize x = normalize 
y" makes things a lot easier.



In principle, what I would like is to have a full stack of algebraic 
structures in HOL-Algebra and a full stack of algebraic structures as 
type classes built on top of that, but I don't think that's going to happen.


I think the best approach at the moment is to gradually flesh out the 
existing hierarchy (like Florian and I have already done with 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 should require an algebraic_semidom [...]
Factorial rings (also known as unique factorisation domains) usually
[...]
[...] (somewhat non-standard) normalization_semidom.

My general impression is that it would be good if the algebraic
hierarchy that is part of standard Isabelle/HOL could follow standard
mathematical definitions and nomenclature more closely.

Best,
Tjark



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Factorial ring

[Manuel Eberl]

"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 commutative semiring.


Factorial rings (also known as unique factorisation domains) usually 
demand that any non-zero element can be written as a (finite) product of 
prime factors and a unit. This representation is necessarily unique 
modulo associativity/commutativity.


Intuitively, I would think that in a normalization_semidom, this implies 
that every non-zero element only has finitely many normalised divisors, 
but I am not completely sure about this. However, this would imply that 
your current definition is, in fact, equivalent to the standard 
mathematical one, at least in the context of the (somewhat non-standard) 
normalization_semidom.



Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] buildall inconsistency

[Manuel Eberl]

I just successfully built the entire distribution and the entire AFP. 
(Isabelle a3c7bd201da7 / AFP 6d199a5)


I also removed the rogue "Euclidean Ring" definition and orphaned 
instances in Echelon_Form, but I think that Echelon_Form, Hermite, 
Algebraic_Numbers and the related 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.tum.de> wrote:

Yes, this has something to do with my ongoing changes to Euclidean Rings and 
related stuff. Everything in the distribution already works again and, as for 
the AFP, I'm on it.

I've removed all of the redundant facts in Euclidean_Algorithm and moved all 
the facts that are not specific to Euclidean Rings to semiring_gcd and 
ring_gcd. I also took care of the appropriate subclass instances and fixed code 
generation for Gcd/Lcm.

Most importantly, I also adapted all the AFP entries that use the polynomial 
GCD to work with the GCD from Euclidean_Algorithm instead of their own 
instances.

We should be able to move Euclidean_Algorithm out of Number_Theory and into the 
main HOL soon.




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Regression in Approximation – Does this belong into NEWS?

[Manuel Eberl]

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 should 
also be put into NEWS/CONTRIBUTORS.


(I have more changes to ‘approximation’ in my pipeline, but these are 
new features and performance improvements, which can wait until after 
the release, but I deemed it important to fix this regression after it 
already made it into the last release)



Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP status

[Manuel Eberl]

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


On 13/01/16 08:56, Andreas Lochbihler wrote:

Applicative_Lifting and Stern_Brocot now (AFP/1c0036f62a32) work with
Isabelle/adcaaf6c9910.

Andreas

On 13/01/16 00:06, Makarius wrote:

The AFP status is much better than last week, but these sessions are
still broken
(Isabelle/7355fd313cf8 and AFP/87337b54f3eb):

   Applicative_Lifting
   Stern_Brocot
   Sturm_Tarski

In this hot phase of release preparation, we need things continuosly
working.


 Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

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 (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"

If I delete this rule, everything works again. I then tried the 
following, which also produces the same error:


lemma binomial_code [code]:
"n choose k = (if k ≤ n then fact n div (fact k * fact (n - k)) else 0)"


The following two, on the other hand, work:

lemma binomial_code [code]:
"0 choose k = (if k = 0 then 1 else 0)"
"Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"

lemma binomial_code [code]:
"n choose k = (if k = 0 then 1 else if n = 0 then 0 else ((n - 1) choose 
(k - 1)) + ((n - 1) choose k))"



So I thought maybe the "fact" is the problem, but the following works as 
well, even though it contains "fact":


lemma binomial_code [code]:
  "n choose k =
 (if k = 0 then 1 else if n = 0 ∧ fact n = fact n then 0 else ((n - 
1) choose (k - 1)) + ((n - 1) choose k))"



Does anybody have any idea what is going on here?


Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

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 also 
do not understand why "export_code … checking" puts everything in a 
single module and if that perhaps has anything to do with it. If I 
simply do "export_code" (without "checking" and "module_name"), the 
problem does /not/ occur. (another completely different problem occurs, 
something about implicits and Typereps)


From what I have seen so far, it seems like there are some lingering 
issues with code generation in general and Codegenerator_Test in 
particular that my rather innocuous change exposed, and that simply 
deleting that one code equation that I added is not the solution we want 
(not even in the short term).


Moreover, at least one AFP entry (namely Rene Thiemann's 
Algebraic_Numbers) crucially depends on a similar code equation for 
"binomial", which causes the exact same problem. We could just leave 
this orphaned code equation in the AFP for now, but that does not strike 
me as a good solution either.



Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

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 and Codegenerator_Test in 
particular that my rather innocuous change exposed, and that simply 
deleting that one code equation that I added is not the solution we 
want (not even in the short term).


I generally agree that things need to be done right, but for the 
moment (3201ddb00097 and after) the main priority is to get back to a 
repository where "isabelle build -a" works.  There are already several 
changes pushed on top of the bad state, which easily leads into a 
situation that takes a long time to disentangle.


I have myself various changes waiting and cannot move forward now, 
neither on main Isabelle nor AFP.



Makarius



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Manuel Eberl]

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 and adapt the AFP entry accordingly.


(I needed this for Liouville_Numbers)


As for the binomial numbers: that looks a bit suboptimal to me. I would 
have expected something like "listprod [k+1..n] div fact (n - k)" plus 
an additional check if "2*k >= n", reducing "n choose k" to "n choose (n 
- k)" if appropriate.


(Not sure what code generation makes of "listprod [k+1..n]", a 
code_unfold rule to compute this efficiently with an accumulator and 
without constructing the list explicitly might be required. Same for 
"fact".)



Cheers,

Manuel


On 11/01/16 09:57, Thiemann, Rene wrote:

Dear all,

there are some changes I would like to add for the upcoming release. It would 
be nice, if someone can integrate them:

- improved code equations for binomial coefficients and certain 
divmod-algorithms.

   (cf. 
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html)

- change type in definition and lemmas about pderiv from real to arbitrary 
fields, or even more general, cf. lines starting with
   (* TODO: inform Isabelle developers *) in 
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html

- change type of divides_degree from complex to 'a :: idom, cf beginning of
   
http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html

Moreover, everything of

http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_*
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_*

can freely be moved from the AFP into the distribution, where I ask the 
developers to judge which parts
belong in the distribution and which are too specific, etc.


With best regards,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Manuel Eberl]

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 you’re right that one can improve it 
by using an inline-version of listprod [k+1..n], but even the version 
that is mentioned in Algebraic_Numbers/Improved_Code_Equations.html is 
by far better than the current setup, since that just uses the 
recursive direct definition of binomial. (I noticed this since I got 
timeouts in my experiments with algebraic numbers and one of the 
culprits was binomial!)


I suggest this:


function fold_atLeastAtMost_nat where
  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
 (if a > b then acc else fold_atLeastAtMost_nat f (a+1) 
b (f a acc))"

by pat_completeness auto
termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto

lemma fold_atLeastAtMost_nat:
  assumes "comp_fun_commute f"
  shows   "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
using assms
proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)
  case (1 f a b acc)
  interpret comp_fun_commute f by fact
  show ?case
  proof (cases "a > b")
case True
thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto
  next
case False
with 1 show ?thesis
  by (subst fold_atLeastAtMost_nat.simps)
 (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)
  qed
qed

lemma setprod_atLeastAtMost_code:
  "setprod f {a..b} = fold_atLeastAtMost_nat (λa acc. f a * acc) a b 1"
proof -
  have "comp_fun_commute (λa. op * (f a))"
by unfold_locales (auto simp: o_def mult_ac)
  thus ?thesis
by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
qed

lemma fact_altdef': "fact n = of_nat (∏{1..n})"
  by (induction n)
 (simp_all add: setprod_nat_ivl_Suc' of_nat_mult [symmetric] 
One_nat_def [symmetric]

   del: of_nat_Suc of_nat_add of_nat_mult One_nat_def)

lemma fact_code [code]:
  "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: 
semiring_char_0)"

proof -
  have "fact n = (of_nat (∏{1..n}) :: 'a)" by (simp add: fact_altdef')
  also have "∏{1..n} = ∏{2..n}"
by (intro setprod.mono_neutral_right) auto
  also have "… = fold_atLeastAtMost_nat (op *) 2 n 1"
by (simp add: setprod_atLeastAtMost_code)
  finally show ?thesis .
qed

lemma binomial_code [code]:
  "(n choose k) =
  (if k > n then 0
   else if 2 * k > n then (n choose (n - k))
   else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
proof -
  {
assume "k ≤ n"
hence "{1..n} = {1..n-k} ∪ {n-k+1..n}" by auto
hence "(fact n :: nat) = fact (n-k) * ∏{n-k+1..n}"
  by (simp add: setprod.union_disjoint fact_altdef_nat)
  }
  thus ?thesis by (auto simp: binomial_altdef_nat mult_ac 
setprod_atLeastAtMost_code)

qed
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Manuel Eberl]

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 also noticed the ring_gcd instance for polynomials. Finalising the 
changes to the GCD class hierarchy and updating the AFP entries that 
rely on half-finished versions of this change (such as Echelon_Form) is 
something that I should probably take care of soon, but definitely not 
before the 2016 release – hopefully before the 2017 one.


Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

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 code equation exactly causes the problem 
tomorrow. If all else fails, I'll just comment out changes until it 
works again and leave this matter to be re-examined after the release.



Cheers,

Manuel



On 11/01/16 18:16, Lawrence Paulson wrote:

I have finally installed my great mass of new material, but when I try to test 
it, it fails as shown below. I can’t imagine what I could have done to trigger 
such an error. Nearly all of my changes are confined to Multivariate_Analysis. 
Does anybody have an idea what could be going on here?

Larry

Running HOL-Codegenerator_Test ...

HOL-Codegenerator_Test FAILED
(see also 
/Users/lp15/isabelle/Repos/heaps/polyml-5.6_x86-darwin/log/HOL-Codegenerator_Test)

^
ROOT.scala:17271: error: ambiguous implicit values:
  both method semiring_char_0_nat in object Generated_Code of type => 
Generated_Code.semiring_char_0[Generated_Code.nat]
  and method semiring_div_nat in object Generated_Code of type => 
Generated_Code.semiring_div[Generated_Code.nat]
  match expected type Generated_Code.power[Generated_Code.nat]
   power[nat](cb, ca) else zero_nata())
 ^
10 errors found

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the release

[Manuel Eberl]

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


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the release

[Manuel Eberl]

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 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 Gamma function and the
Generalised Binomial Theorem.

The work itself is already, all that remains is to merge it into the
distribution. I put the files in this repository if anyone wants to look
at them: https://github.com/3of8/isabelle_summation

The only files that require any real merging (as opposed to just copying
the file into the distribution) are Summation.thy,
Extended_Real_Lemma_Bucket.thy, and Liminf_Limsup_Lemma_Bucket.thy. The
file "Concave.thy" is not required by the rest and does not need to be
merged.


None of this really has to end up in Isabelle2016; I can also wait for
the next release. My plan was to meet with Johannes and Fabian after the
holidays and ask them for their opinions on this material.


Cheers,

Manuel


On 01/01/16 20:24, Makarius wrote:

Isabelle2016-RC0 is published, but we are still in normal incremental
change mode on the isabelle-dev repository.

This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS, and
the website.


Are there bigger changes still in the pipeline?  Larry are you finished
with the ports from HOL Light, as far as Isabelle2016 is concerned?

Depending on that, the fork point for the release will be a bit sooner
or later.  Lets say in about 2 weeks. Hopefully, Oracle manages to
deliver the next Java 8 update in 3 weeks, as scheduled.


 Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the release

[Manuel Eberl]

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 Gamma function and the 
Generalised Binomial Theorem.


The work itself is already, all that remains is to merge it into the 
distribution. I put the files in this repository if anyone wants to look 
at them: https://github.com/3of8/isabelle_summation


The only files that require any real merging (as opposed to just copying 
the file into the distribution) are Summation.thy, 
Extended_Real_Lemma_Bucket.thy, and Liminf_Limsup_Lemma_Bucket.thy. The 
file "Concave.thy" is not required by the rest and does not need to be 
merged.



None of this really has to end up in Isabelle2016; I can also wait for 
the next release. My plan was to meet with Johannes and Fabian after the 
holidays and ask them for their opinions on this material.



Cheers,

Manuel


On 01/01/16 20:24, Makarius wrote:

Isabelle2016-RC0 is published, but we are still in normal incremental
change mode on the isabelle-dev repository.

This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS, and
the website.


Are there bigger changes still in the pipeline?  Larry are you finished
with the ports from HOL Light, as far as Isabelle2016 is concerned?

Depending on that, the fork point for the release will be a bit sooner
or later.  Lets say in about 2 weeks. Hopefully, Oracle manages to
deliver the next Java 8 update in 3 weeks, as scheduled.


 Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev