Re: [isabelle-dev] AFP status

[Andreas Lochbihler]

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

Re: [isabelle-dev] HOL-Codegenerator_Test error

[Andreas Lochbihler]

Dear Manuel,

I have not tried this explicitly, but it looks like the standard problem with type classes 
in Scala (see section 7.1 in the code generator tutorial). Probably the problematic code 
equations use two type classes with an operation inherited from the same anchestor. The 
error message in the start of this thread hints at this problem. So you best introduce a 
special type class for Scala (as has already been done for others in the code generator 
tests).


Hope this helps,
Andreas

On 12/01/16 09:56, Manuel Eberl wrote:

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

___
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

[Thiemann, Rene]

Hi Manuel,

> I added the efficient code equations for fact and binomial, and similar ones 
> for pochhammer and gbinomial.
> 
> I also adapted everything from Square_Free_Factorization and 
> Missing_Polynomial that seemed to be of general interest to me (especially 
> the generalisation of the type of pderiv).

thanks a lot; in the meantime, I deleted this material from the AFP-entries.

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

The absence of the ring_gcd instance for polynomials is strange from my 
perspective: In Isabelle 2015 we had

  instantiation poly :: (field) gcd

where the gcd-class contained the important properties of a gcd.

In Isabelle 2016-RC0 there also is  

  instantiation poly :: (field) gcd

but now the gcd-class is purely syntactic. Here, to get the same properties of 
a gcd (and more), the corresponding instance would be

  instantiation poly :: (field) semiring_gcd   (or ring_gcd) 

So why should the small proof below be not integrated for the 2016 release? 
Otherwise, there
is no class-based gcd for polynomials available for 2016, in contrast to 2015.

instance poly :: (field) ring_gcd
proof 
  fix a b :: "'a poly"
  show "normalize (gcd a b) = gcd a b" by (simp add: normalize_poly_def 
poly_gcd_monic)
  show "lcm a b = normalize (a * b) div gcd a b" 
  proof (cases "a * b = 0") 
case False
show ?thesis unfolding lcm_poly_def normalize_poly_def
by (subst div_smult_right, insert False, auto simp: div_smult_left)
   (metis coeff_degree_mult divide_divide_eq_left divide_inverse_commute 
inverse_eq_divide)
  next
case True
thus ?thesis by (metis div_0 lcm_poly_def normalize_0)
  qed
qed auto


Cheers,
René
___
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] Isabelle2016-RC0: potential changes

[Makarius]

On Tue, 12 Jan 2016, Manuel Eberl wrote:

 So why should the small proof below be not integrated for the 2016 

release?

This is probably a question for Florian. I introduced Euclidean rings to 
allow a more systematic derivation of (constructive) GCDs about two years ago 
or so.


As for the release, perhaps Florian can comment on whether anything 
speaks against moving this instance into the Polynomial theory.


I can't say anything specific about these parts of the library, but 
generally I would be glad to see this sorted out for this release.  There 
is approximately all of this week left to add such small things -- and to 
get AFP into proper shape as well.



Makarius
___
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

[Makarius]

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] HOL-Codegenerator_Test error

[Lars Hupel]

(Take the following with a grain of salt, it is the result of a cursory
investigation.)

As far as I can tell the current problem is a variation of §7.1.

Here's an excerpt from the error log:

[error] /tmp/foo/foo.scala:5687: ambiguous implicit values:
[error]  both method semiring_char_0_nat in object ROOT of type =>
ROOT.semiring_char_0[ROOT.nat]
[error]  and method semiring_div_nat in object ROOT of type =>
ROOT.semiring_div[ROOT.nat]
[error]  match expected type ROOT.power[ROOT.nat]
[error]  less_eq_nat(power[nat](m,
nat_of_integer(BigInt(2))),
[error]^

The affected function is:

def sqrt(n: nat): nat =
  Max[nat](filter[nat](((m: nat) =>
 less_eq_nat(power[nat](m,
nat_of_integer(BigInt(2))),
  n)),
seta[nat](upt(zero_nata, Suc(n)

As can be seen, it is not parameterized over types. There are actually
two legitimate ambiguous implicit values (with the inherent ambiguity
stemming from the export scheme of instances to Scala*).

The solution here might very well be to "close the diamond", but I fail
to understand how this compiled in the first place.

Cheers
Lars


* there is the possibility of improving the scheme to avoid the present
problem, but not the problem described in §7.1**
** if we want to fix §7.1 once and for all, the code generator needs to
disambiguate manually
___
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

[Lawrence Paulson]

I had a problem like this last year. Unlike a broken proof, they seem almost 
impossible to fix. Something’s fragile about this setup.
Larry

> On 12 Jan 2016, at 11:04, Manuel Eberl  wrote:
> 
> 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

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

Re: [isabelle-dev] Impossible_Geometry

[Johannes Hölzl]

Am Dienstag, den 12.01.2016, 13:48 + schrieb Lawrence Paulson:
> This AFP entry no longer works. I think that the culprit is recent
> changes affecting the metric_space type class. See attachment.
> 
> Larry


Ah, sorry I overlooked this. I will fix it.

 - Johannes
___
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

[isabelle-dev] AFP status

[Makarius]

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] NEWS: better resource usage on all platforms

[Makarius]

This refers to the NEWS update in adcaaf6c9910.

In the past few months there have been many changes on both the ML and 
Scala side to make more of available resources, and to avoid demanding too 
much of them.  In the coming weeks it is important to keep a keen eye on 
how it works in practice.



The latest and cheapest trick is

changeset:   62115:57895801cb57
user:wenzelm
date:Sun Jan 10 23:25:11 2016 +0100
files:   etc/options src/Pure/PIDE/session.scala
description:
prune old versions more often, to reduce overall heap requirements;


Users with a private editor_prune_delay in etc/preferences should follow 
that change.



Makarius

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