Builds keep failing · Mirror: Isabelle Development Mailing List

Stream: Mirror: Isabelle Development Mailing List

Topic: Builds keep failing

Email Gateway (Apr 29 2025 at 10:49):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
… With the error "Value or constructor (string_of_goal) has not been declared in structure Goal_Display”

This looks easy to fix, isn't it?

Larry

Email Gateway (Apr 29 2025 at 11:23):

From: Makarius <makarius@sketis.net>
On 29/04/2025 12:48, Lawrence Paulson via isabelle-dev wrote:

… With the error "Value or constructor (string_of_goal) has not been declared in structure Goal_Display”

Oops, I've forgotten to push some local changes. See now AFP/022cb76fe2b4.

Makarius

Email Gateway (May 31 2026 at 07:56):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

Does anyone know what is going on here? The repeated failures are getting distracting.
Larry

Estimated 0:02:32 build time with generation scheme (default heuristic) (took 0.015s)
Running Isabelle-Solidity (started 0:01:50 on of1-proof_schedule+0-15) ...
Isabelle-Solidity FAILED (see also "isabelle build_log -H Error Isabelle-Solidity")
...
*** Reason:
*** Can't unify Proof.context to 'a -> thm list -> context
*** (Incompatible types)
*** ML error (line 154 of "~~/dirs/AFP/thys/Isabelle-Solidity/Specification.ML"):
*** Type error in function application.

Email Gateway (May 31 2026 at 08:40):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

Does anyone know what is going on here? The repeated failures are getting distracting.
Larry

Email Gateway (May 31 2026 at 11:14):

From: Makarius <makarius@sketis.net>

On 31/05/2026 09:56, Lawrence Paulson via isabelle-dev wrote:

Does anyone know what is going on here? The repeated failures are getting distracting.
Larry

Estimated 0:02:32 build time with generation scheme (default heuristic) (took 0.015s)
Running Isabelle-Solidity (started 0:01:50 on of1-proof_schedule+0-15) ...
Isabelle-Solidity FAILED (see also "isabelle build_log -H Error Isabelle-Solidity")
...
*** Reason:
*** Can't unify Proof.context to 'a -> thm list -> context
*** (Incompatible types)
*** ML error (line 154 of "~~/dirs/AFP/thys/Isabelle-Solidity/Specification.ML"):
*** Type error in function application.

Looking briefly at the history, I see this change:

changeset: 16628:a4778d4a4355
parent: 16626:9d47a38b2406
user: dmarmsoler
date: Fri May 29 17:58:39 2026 +0100
files: thys/Isabelle-Solidity/Bank.thy thys/Isabelle-Solidity/Casino.thy
thys/Isabelle-Solidity/Contract.thy thys/Isabelle-Solidity/Data.ML
thys/Isabelle-Solidity/Invariant.ML thys/Isabelle-Solidity/LICENSE
thys/Isabelle-Solidity/Memory.thy thys/Isabelle-Solidity/ROOT
thys/Isabelle-Solidity/SimpleAuction.thy thys/Isabelle-Solidity/Solidity.thy
thys/Isabelle-Solidity/Specification.ML thys/Isabelle-Solidity/State.thy
thys/Isabelle-Solidity/State_Monad.thy thys/Isabelle-Solidity/Stores.thy
thys/Isabelle-Solidity/Token.thy thys/Isabelle-Solidity/Unit_Tests.thy
thys/Isabelle-Solidity/Utils.ML thys/Isabelle-Solidity/Verification.ML
thys/Isabelle-Solidity/Voting.thy thys/Isabelle-Solidity/WP.thy
thys/Isabelle-Solidity/document/orcidlink.sty
thys/Isabelle-Solidity/document/root.tex
description:
Major improvements to Isabelle-Solidity

The semantics was updated to be compliant with a more recent version of
Solidity (v0.8.25).
In addition to external functions it now also supports internal functions.
In addition to the verification of invariants, it now also supports the
verification of (multiple) pre/post-conditions for functions.
Type consistency is added as pre-condition for functions.

See now:

changeset: 16635:bfc13a2200a1
user: wenzelm
date: Sun May 31 12:57:00 2026 +0200
files: thys/Isabelle-Solidity/Specification.ML
thys/Isabelle-Solidity/Verification.ML
description:
make Isabelle-Solidity actually work with current Isabelle/6f7803fbcc0f
(amending a4778d4a4355);

Makarius

Last updated: Jun 04 2026 at 18:19 UTC