Stream: Mirror: Isabelle Development Mailing List

Topic: repeated build failures

view this post on Zulip Email Gateway (Sep 19 2026 at 10:40):

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

There’s a markup error in "~~/src/HOL/SMT_CVC_Real.thy”. It’s been there for quite a while. Does anybody know who is in charge of this?

Larry

view this post on Zulip Email Gateway (Sep 19 2026 at 16:03):

From: Makarius <makarius@sketis.net>

On 19/09/2026 12:40, Lawrence Paulson via isabelle-dev wrote:

There’s a markup error in "~~/src/HOL/SMT_CVC_Real.thy”. It’s been there for quite a while. Does anybody know who is in charge of this?

For such document failures, anybody is in charge who clearly understands the
problem (which is trivial). See now:

changeset: 85640:9db2120d1f68user: wenzelm
date: Sat Sep 19 15:34:41 2026 +0200
files: src/HOL/SMT_CVC_Real.thy
description:
proper document antiquotations for quasi-formal text (amending 2d8973a32588);

Makarius

Last updated: Oct 05 2026 at 16:54 UTC