Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-14 Thread 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

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread 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

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread 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

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread 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

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread 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

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread 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.

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread 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 >

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread 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

[isabelle-dev] HOL-Codegenerator_Test error

2016-01-11 Thread 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?

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-11 Thread 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

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-11 Thread 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