Re: [isabelle-dev] HOL-Codegenerator_Test error

[Florian Haftmann]

As Andreas and Lars have pointed out, this is the issue described in
§7.1 in the tutorial on code generation.

I will have a look at this after the release.

Florian

Am 12.01.2016 um 23:51 schrieb Makarius:
> On Tue, 12 Jan 2016, Manuel Eberl wrote:
> 
>> I commented out the code equation in question and
>> HOL-Codegenerator_Test runs through again.
> 
> Thanks.
> 
> For the historical record: that is Isabelle/18a217591310.
> 
> (Mercurial changeset ids allow to talk about history in a timeless and
> stateless manner.)
> 
> 
> Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
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] 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

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

[Lawrence Paulson]

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

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

[Makarius]

On Mon, 11 Jan 2016, Manuel Eberl wrote:

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.


Just a reminder of the normal routine: push to the Isabelle repository 
always requires a full "isabelle build -a" -- there is no way around it.


It would be also nice to have a continously working AFP, as we are 
approaching the release.



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