Builds keep failing

[Makarius]

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