Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Failure of AFP/Proof_Strategy_Language

view this post on Zulip Email Gateway (Oct 26 2024 at 20:04):

From: Makarius <makarius@sketis.net>
In Isabelle/d3c0734059ee + AFP/4082096ade5a we have a failure of
AFP/Proof_Strategy_Language:

Proof_Strategy_Language FAILED (see also "isabelle build_log -H Error
Proof_Strategy_Language")
*** empty sequence. no proof found.
*** At command "find_proof" (line 88 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 34 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 101 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 16 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 29 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 22 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")

The parent Isabelle/0c9075bdff38 appears to be fine, so it is probably due to
the changes in Sledgehammer in d3c0734059ee.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Oct 28 2024 at 08:39):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Makarius,

Yes, my (actually: Lukas Bartl's, under my supervision) change to Sledgehammer (d3c0734059ee) is probably the issue.

Sledgehammer is an end user tool. It should be possible to change its output without breaking things. So I'm not a big fan of the "Proof_Strategy_Language" entry's existence in the AFP. But since it's there, maybe we could ask its developer to fix it?

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 26. Oct 2024, at 22:03, Makarius <makarius@sketis.net> wrote:

In Isabelle/d3c0734059ee + AFP/4082096ade5a we have a failure of AFP/Proof_Strategy_Language:

Proof_Strategy_Language FAILED (see also "isabelle build_log -H Error Proof_Strategy_Language")
*** empty sequence. no proof found.
*** At command "find_proof" (line 88 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 34 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 101 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 16 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 29 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 22 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")

The parent Isabelle/0c9075bdff38 appears to be fine, so it is probably due to the changes in Sledgehammer in d3c0734059ee.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

smime.p7s

view this post on Zulip Email Gateway (Oct 28 2024 at 10:00):

From: Peter Lammich <lammich@in.tum.de>

On 28/10/2024 09:39, Jasmin Blanchette wrote:

Hi Makarius,

Yes, my (actually: Lukas Bartl's, under my supervision) change to
Sledgehammer (d3c0734059ee) is probably the issue.

Sledgehammer is an end user tool. It should be possible to change its
output without breaking things. So I'm not a big fan of the
"Proof_Strategy_Language" entry's existence in the AFP. But since it's
there, maybe we could ask its developer to fix it?

Doesn't sledgehammer have an API?

--

Peter

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 26. Oct 2024, at 22:03, Makarius <makarius@sketis.net> wrote:

In Isabelle/d3c0734059ee + AFP/4082096ade5a we have a failure of
AFP/Proof_Strategy_Language:

Proof_Strategy_Language FAILED (see also "isabelle build_log -H Error
Proof_Strategy_Language")
*** empty sequence. no proof found.
*** At command "find_proof" (line 88 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 34 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 101 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 16 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 29 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
*** empty sequence. no proof found.
*** At command "find_proof" (line 22 of
"~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")

The parent Isabelle/0c9075bdff38 appears to be fine, so it is
probably due to the changes in Sledgehammer in d3c0734059ee.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Oct 28 2024 at 10:21):

From: Fabian Huch <huch@in.tum.de>
On 10/28/24 10:59, Peter Lammich wrote:

On 28/10/2024 09:39, Jasmin Blanchette wrote:

Hi Makarius,

Yes, my (actually: Lukas Bartl's, under my supervision) change to
Sledgehammer (d3c0734059ee) is probably the issue.

Sledgehammer is an end user tool. It should be possible to change its
output without breaking things. So I'm not a big fan of the
"Proof_Strategy_Language" entry's existence in the AFP. But since
it's there, maybe we could ask its developer to fix it?

Doesn't sledgehammer have an API?

It looks like the entry uses the API, but then prints the output and
re-parses it (instead of working with typed data), which is of course bad.

Fabian

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Feb 01 2025 at 20:19 UTC