I have two items of interest for the coming release.
There is some interest here at Data61 (NICTA that was) in having a
localised record package in Isabelle-2016. I've done the initial
implementation and got the parts of the package I understand working
within locales etc, but something goes
Hi Thomas,
> There is some interest here at Data61 (NICTA that was) in having a
> localised record package in Isabelle-2016. I've done the initial
> implementation and got the parts of the package I understand working
> within locales etc, but something goes wrong with the code generation
>
Hi Johannes, hi Andreas,
the core of the problem is that dictionaries are always generated for
type class instances, even if the operations therein are never referred
to. Is this the first time that we have such a situation, or are there
more examples (e.g. in the AFP)? If yes, the code
Hi Rene,
>> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
>> thus very hardly different from syntactic classes, so there is no loss
>> of generality here.
>
> I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015
> have
> the three essential
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 all,
>
> I have already some post-release patches in the pipeline which would add
> this instance anyway. So, there is no demand for action here at the moment.
>
> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
> thus very hardly different from syntactic classes,
Hi all,
> 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.
>
> Since then, Florian cleaned this up and improved it a lot, but from what
> I gathered, there is much to be done yet. I
On Thu, 14 Jan 2016, Florian Haftmann wrote:
Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
thus very hardly different from syntactic classes, so there is no loss
of generality here.
I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015
have
the
On Thu, 14 Jan 2016, Thomas Sewell wrote:
The second proposal is probably more contentious. I'm hoping to
reimplement a tool we had in the past that speeds up proof maintenance
work by selectively skipping proofs that are very likely to succeed. To
support that, I'm proposing adding a couple
On Thu, 14 Jan 2016, Florian Haftmann wrote:
Hi Thomas,
There is some interest here at Data61 (NICTA that was) in having a
localised record package in Isabelle-2016. I've done the initial
implementation and got the parts of the package I understand working
within locales etc, but something
On Thu, 14 Jan 2016, Thomas Sewell wrote:
Right. There was a plan here to investigate before the release, but the
timing didn't work out.
You mean *after* the release. Bigger changes are always reconsidered
after lift-off of release N, to be included in release N + 1 or N + k for
k >= 2.
AFAIK, it is the first time we have such a situation. We have two cases
I'm aware of: "open" in topological_space and "uniformity" in
uniform_space. Up to now we could just remove all code equations from
open as it is a predicate and doesn't produce any problem with the
dictionary construction.
12 matches
Mail list logo
