Email Gateway (Feb 28 2024 at 13:41): Email Gateway (Feb 28 2024 at 13:41):From: Peter Lammich <lammich@in.tum.de>
Hello List,
I ran into a problem, that Isabelle (on Ubuntu 22.04, 12 core processor)
would sometimes report a "Duplicate use of derivation identity" error at
the very end of the theory file. This behavior seems to be
non-deterministic, i.e., sometimes it occurs, and when editing the file,
it sometimes does not occur. Also, it seems to depend on the size of the
theory AND the naming of the theorems. When I tried to compose a small
counterexample, I couldn't reproduce the error.
Before I invest more work: is this error known? or expected given the
naming of my theorems? If not, shall I try to compose a (smallish)
example that reproduces it?
The offending theorems seem to be:
lemma gen_fri_match_step1_1: ...
lemma gen_fri_match_step1_2: ...
lemmas gen_fri_match_step1 = gen_fri_match_step1_1 gen_fri_match_step1_2
Error message, marked roughly at end of theory, but the red squiggle is
a few characters behind the "end" command, see screenshot. Also, the
error message does not occur in the output window.
Full error message:
"exception THM 0 raised (line 107 of "global_theory.ML"): Duplicate use
of derivation identity for Separation_Logic_ToolsX.gen_fri_match_step1_1
vs. Separation_Logic_ToolsX.gen_fri_match_step1(1)"
Email Gateway (Feb 28 2024 at 13:51):From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Hello List,
Update: the error actually occurs deterministically (bit it may take a
second or two until it is displayed by jedit).
Also, it doesn't depend on the theory size, here is a small example:
theory Test
imports Main
begin
lemma n_1: "True" by simp
lemma n_2: "True" by simp
lemmas n = n_1 n_2
end
Again: is this expected? documented? and why is the error display that
strange (not in output window, red-squiggle behind end?)
Email Gateway (Feb 28 2024 at 14:02):From: Fabian Huch <huch@in.tum.de>
I don't know exactly where the problem is triggered, but I suspect the
conflict comes from Thm_Name.flatten:
If you give it a non-singleton fact (e.g., "gen_fri_match_step1(1)"), it
will flatten with with an underscore ("gen_fri_match_step1_1") -- which
is already taken by the previous lemmas in your naming scheme.
Fabian
Email Gateway (Feb 28 2024 at 19:31):From: Lawrence Paulson <lp15@cam.ac.uk>
Probably we should change this behaviour. I’ve seen the “flattened” names in some trace outputs, but they aren’t even accepted. Maybe they should be “flattened” to n(1), etc.
Larry
Email Gateway (Feb 28 2024 at 19:58):From: Makarius <makarius@sketis.net>
On 28 Feb 2024, at 13:53, Fabian Huch <huch@in.tum.de> wrote:
I don't know exactly where the problem is triggered, but I suspect the conflict comes from Thm_Name.flatten:
If you give it a non-singleton fact (e.g., "gen_fri_match_step1(1)"), it will flatten with with an underscore ("gen_fri_match_step1_1") -- which is already taken by the previous lemmas in your naming scheme.
Last updated: Apr 29 2024 at 04:18 UTC