Stream: Mirror: Isabelle Development Mailing List

Topic: AFP broken

view this post on Zulip Email Gateway (Jun 01 2025 at 12:13):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
isabelle: 0a3d61228714 tip
afp: fe4648e3837e+ tip

Starting job user/1748 at Sun Jun 1 14:11:03 GMT+2 2025, on cluster
Using Isabelle/0a3d61228714
Using AFP
isabelle build -A: -H of1-proof_classic:hostname\=of1.proof.cit.tum.de,user\=cluster,jobs\=2,threads\=8 -H of2-proof_classic:hostname\=of2.proof.cit.tum.de,user\=cluster,jobs\=2,threads\=8 -H of3-proof_classic:hostname\=of3.proof.cit.tum.de,user\=cluster,jobs\=2,threads\=8 -H of4-proof_classic:hostname\=of4.proof.cit.tum.de,user\=cluster,jobs\=2,threads\=8 -H se1_classic:hostname\=se1.proof.cit.tum.de,user\=cluster,jobs\=2,threads\=8 -H se2_classic:hostname\=se2.proof.cit.tum.de,user\=cluster,jobs\=3,threads\=8 -H se3_classic:hostname\=se3.proof.cit.tum.de,user\=cluster,jobs\=3,threads\=8 -H se4_classic:hostname\=se4.proof.cit.tum.de,user\=cluster,jobs\=3,threads\=8 -a
*** Cannot load theory "First_Order_Clause.Ground_Context"
*** The error(s) above occurred for theory "First_Order_Clause.Ground_Context"
*** (required by "SCL_Simulates_Ground_Resolution.Simulation_SCLFOL_ORDRES" via "SCL_Simulates_Ground_Resolution.Background" via "SCL_Simulates_Ground_Resolution.Ground_Ordered_Resolution") (line 6 of "/tmp/ssh-5JJ4VTdEF9bF/dirs/AFP/thys/SCL_Simulates_Ground_Resolution/Ground_Ordered_Resolution.thy")
*** Cannot load theory "First_Order_Clause.Ground_Context"
*** No such file: "First_Order_Clause.Ground_Context"
*** The error(s) above occurred in session "SCL_Simulates_Ground_Resolution" (line 2 of "/tmp/ssh-5JJ4VTdEF9bF/dirs/AFP/thys/SCL_Simulates_Ground_Resolution/ROOT")
Job ended at Sun Jun 1 14:12:04 GMT+2 2025, with status failed

See also
https://build.proof.cit.tum.de/build?id=8a367e07-edde-40ca-ae13-cc521072025f

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

view this post on Zulip Email Gateway (Jun 01 2025 at 18:31):

From: Makarius <makarius@sketis.net>
On 6/1/25 14:12, Florian Haftmann wrote:

isabelle: 0a3d61228714 tip
afp: fe4648e3837e+ tip

I see a total existence failure here:

changeset: 15733:7262c283575c
tag: tip
user: Balazs Toth <balazs.toth.isny@gmail.com>
date: Fri May 30 19:10:18 2025 +0200
summary: Superposition_Calculus: Adapt ground critical pairs from
First_Order_Rewriting + Make calculus independent of term data types

Using its parent works: Isabelle/06aac7eaec29 + AFP/b227c97a92f5.

Makarius

Last updated: Jul 12 2025 at 16:25 UTC