Email Gateway (Feb 05 2025 at 16:28): Email Gateway (Feb 05 2025 at 16:28):From: Peter Lammich <lammich@in.tum.de>
Porting Isabelle-LLVM was mostly straightforward.
(https://github.com/lammich/isabelle_llvm/tree/2025)
Minor points:
* make_simproc, it's hard to find what the possible values for the new
kind= field are.
* Some change to the simpset caused a single proof on real numbers to
break down without easy fix. Adding field_simps and sledgehammer
helped at the end, though. Had no time to further investigate, but
probably minor problem as it affected only a single proof.
* There used to be a lemma
Divides.unique_euclidean_semiring_numeral_class.div_positive: ⟦0 <
?b; ?b ≤ ?a⟧ ⟹ 0 < ?a div ?b. In the new setup, this exists only as
an equivalence. I used div_greater_zero_iff[THEN iffD2] to (roughly)
get the old one back.
Not relevant for Isabelle-release:
Changeset 6ded6efc058a for AFP/Automatic_Refinement/Lib/Refine_Util.thy:
this has added an unused ctxt-parameter to the WITH_concl combinator.
--
Peter and Bram
Email Gateway (Feb 07 2025 at 14:21):From: Makarius <makarius@sketis.net>
On 05/02/2025 17:21, Peter Lammich wrote:
Porting Isabelle-LLVM was mostly straightforward. (https://github.com/lammich/
isabelle_llvm/tree/2025)
Thank you for testing, and following the release train at this stage already.
Minor points:
* make_simproc, it's hard to find what the possible values for the new kind=
field are.
That is a rather old low-level entry point. Already some years ago, I've
introduced an ML antiquotation that resembles the Isar command
'simproc_setup'. Thus it becomes independent of minor changes in the ML
interfaces. See also this changeset
https://isabelle-dev.sketis.net/rISABELLE64973b03b778
changeset: 78806:64973b03b778
user: wenzelm
date: Sat Oct 21 11:24:34 2023 +0200
files: src/HOL/Decision_Procs/langford.ML
src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_replay.ML src/HOL/Tools/int_arith.ML
src/HOL/Tools/numeral_simprocs.ML src/Tools/induct.ML
description:
more standard simproc_setup using ML antiquotation;
Not relevant for Isabelle-release:
Changeset 6ded6efc058a for AFP/Automatic_Refinement/Lib/Refine_Util.thy: this
has added an unused ctxt-parameter to the WITH_concl combinator.
That is indeed pointless, I have removed it again in AFP/265afdb508aa.
The Proof.context got into AFP/6ded6efc058a by accident, because I was
considering to require one for the goal state operations at the bottom of
src/Pure/logic.ML. This did not materialize: these operations are considered
to low-level to observe parameter names seen by the end-user.
Makarius
Last updated: Mar 09 2025 at 12:28 UTC