Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Build of AFP entry PAPP_Impossibility failed


view this post on Zulip Email Gateway (Aug 29 2026 at 14:45):

From: Manuel Eberl <manuel@pruvisto.org>

Hello,

I've been getting a lot of emails like this for the past few weeks. I
can't remember getting these before then. I wonder if some change
happened during that time that affected memory consumption. It seems to
be the either the generation of the SAT instance or the import of the
SAT proof that causes this.

Surprisingly, I don't recall getting a single email about the entry
SWF_Impossibility, which does something very similar but four times
instead of one, and two of the SAT proofs involved are quite a bit
bigger than the one in PAPP_Impossibility.

Manuel

-------- Forwarded Message --------
Subject: Build of AFP entry PAPP_Impossibility failed
Date: Sat, 29 Aug 2026 04:13:16 +0200 (CEST)
From: AFP Build <ci@proof.cit.tum.de>
To: manuel@pruvisto.org

The build for the session PAPP_Impossibility belonging to the AFP entry
PAPP_Impossibility failed.

You are receiving this mail because you are the maintainer of that AFP
entry.

The following information might help you with resolving the problem.

Build log: https://build.proof.cit.tum.de/build?name=presentation%2F764

Isabelle ID: dc45b445012a
AFP ID: 83221a878a3a
Timeout? false
Exit code: 1

Last 50 lines from stdout (if available):

*** Failed to load theory "PAPP_Impossibility.PAPP_Impossibility"
(unresolved "PAPP_Impossibility.PAPP_Impossibility_Base_Case")
*** exception Interrupt_Breakdown raised (line 77 of
"./basis/PolyMLException.sml")
*** At command "local_setup" (line 686 of
"~~/dirs/AFP/thys/PAPP_Impossibility/PAPP_Impossibility_Base_Case.thy")"

Last 50 lines from stderr (if available):

Run out of store - interrupting threads


Last updated: Sep 02 2026 at 16:10 UTC