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
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
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
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
(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
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 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
>
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
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?
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
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
11 matches
Mail list logo