Stream: Mirror: Isabelle Development Mailing List

Topic: Broken AFP/SCL_Simulates_Ground_Resolution

view this post on Zulip Email Gateway (Jan 11 2025 at 20:35):

From: Makarius <makarius@sketis.net>
We have a total existence failure of AFP, due to import of a non-existent theory.

I have disabled the bad session for now, see also:

changeset: 15168:e681bc604fb1
tag: tip
user: wenzelm
date: Sat Jan 11 21:28:06 2025 +0100
summary: disable SCL_Simulates_Ground_Resolution for now: import of
missing theory Superposition_Calculus.Ground_Ctxt_Extra;

Makarius

view this post on Zulip Email Gateway (Jan 12 2025 at 10:17):

From: Martin Desharnais <martin.desharnais@posteo.de>
Hi Makarius,

adapted the AFP entry to Isabelle-devel and AFP-devel.

changeset: 15198:9585bf0cf504
tag: tip
user: desharna
date: Sun Jan 12 10:58:53 2025 +0100
summary: backed out changeset e681bc604fb1 following dca39520060a

changeset: 15197:dca39520060a
user: desharna
date: Sun Jan 12 10:54:01 2025 +0100
summary: adapted SCL_Simulates_Ground_Resolution to Isabelle-devel
and afp-devel

Regards,
Martin

Am 2025-01-11 21:34 schrieb Makarius:

We have a total existence failure of AFP, due to import of a
non-existent theory.

I have disabled the bad session for now, see also:

changeset: 15168:e681bc604fb1
tag: tip
user: wenzelm
date: Sat Jan 11 21:28:06 2025 +0100
summary: disable SCL_Simulates_Ground_Resolution for now: import
of missing theory Superposition_Calculus.Ground_Ctxt_Extra;

Makarius

Last updated: Feb 01 2025 at 20:19 UTC