pkgsrc-WIP-changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
lean4-git: reduce allocations between fork + exec
Module Name: pkgsrc-wip
Committed By: Thomas Klausner <wiz%NetBSD.org@localhost>
Pushed By: wiz
Date: Fri Aug 28 19:14:49 2026 +0200
Changeset: 640d8cbf616661a098fa0d890c279a4a9aa7258d
Modified Files:
lean4-git/Makefile
lean4-git/PLIST
lean4-git/distinfo
lean4-git/patches/patch-src_runtime_process.cpp
lean4-git/patches/patch-stage0_src_runtime_process.cpp
Log Message:
lean4-git: reduce allocations between fork + exec
To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=640d8cbf616661a098fa0d890c279a4a9aa7258d
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
diffstat:
lean4-git/Makefile | 2 +-
lean4-git/PLIST | 238 +++++++++------------
lean4-git/distinfo | 4 +-
lean4-git/patches/patch-src_runtime_process.cpp | 115 +++++++++-
.../patches/patch-stage0_src_runtime_process.cpp | 115 +++++++++-
5 files changed, 320 insertions(+), 154 deletions(-)
diffs:
diff --git a/lean4-git/Makefile b/lean4-git/Makefile
index 833e4aa8da..3f64b8278a 100644
--- a/lean4-git/Makefile
+++ b/lean4-git/Makefile
@@ -47,7 +47,7 @@ SUBST_CLASSES+= cc
SUBST_FILES.cc+= src/Leanc.lean
SUBST_FILES.cc+= src/lake/Lake/Build/Common.lean
SUBST_SED.cc+= -e "s,@LEANC_CC@,${CC},"
-SUBST_SED.cc+= -e "s!@LINKER_FLAGS@!\"${COMPILER_RPATH_FLAG}${PREFIX}/lib\", \"${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean\", \"-lgcc_s\"!"
+SUBST_SED.cc+= -e "s!@LINKER_FLAGS@!\"${COMPILER_RPATH_FLAG}${PREFIX}/lib\", \"${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean\"!"
SUBST_STAGE.cc= pre-configure
SUBST_MESSAGE.cc= Setting compiler path.
diff --git a/lean4-git/PLIST b/lean4-git/PLIST
index b4b33b2d86..3b168925e3 100644
--- a/lean4-git/PLIST
+++ b/lean4-git/PLIST
@@ -7750,6 +7750,12 @@ lib/lean/Lean/Elab/Tactic/Rfl.ir.sig
lib/lean/Lean/Elab/Tactic/Rfl.olean
lib/lean/Lean/Elab/Tactic/Rfl.olean.private
lib/lean/Lean/Elab/Tactic/Rfl.olean.server
+lib/lean/Lean/Elab/Tactic/Rwa.ilean
+lib/lean/Lean/Elab/Tactic/Rwa.ir
+lib/lean/Lean/Elab/Tactic/Rwa.ir.sig
+lib/lean/Lean/Elab/Tactic/Rwa.olean
+lib/lean/Lean/Elab/Tactic/Rwa.olean.private
+lib/lean/Lean/Elab/Tactic/Rwa.olean.server
lib/lean/Lean/Elab/Tactic/Show.ilean
lib/lean/Lean/Elab/Tactic/Show.ir
lib/lean/Lean/Elab/Tactic/Show.ir.sig
@@ -14108,12 +14114,30 @@ lib/lean/Std/Sat/CNF/Dimacs.ir.sig
lib/lean/Std/Sat/CNF/Dimacs.olean
lib/lean/Std/Sat/CNF/Dimacs.olean.private
lib/lean/Std/Sat/CNF/Dimacs.olean.server
+lib/lean/Std/Sat/CNF/Entails.ilean
+lib/lean/Std/Sat/CNF/Entails.ir
+lib/lean/Std/Sat/CNF/Entails.ir.sig
+lib/lean/Std/Sat/CNF/Entails.olean
+lib/lean/Std/Sat/CNF/Entails.olean.private
+lib/lean/Std/Sat/CNF/Entails.olean.server
lib/lean/Std/Sat/CNF/Literal.ilean
lib/lean/Std/Sat/CNF/Literal.ir
lib/lean/Std/Sat/CNF/Literal.ir.sig
lib/lean/Std/Sat/CNF/Literal.olean
lib/lean/Std/Sat/CNF/Literal.olean.private
lib/lean/Std/Sat/CNF/Literal.olean.server
+lib/lean/Std/Sat/CNF/Negation.ilean
+lib/lean/Std/Sat/CNF/Negation.ir
+lib/lean/Std/Sat/CNF/Negation.ir.sig
+lib/lean/Std/Sat/CNF/Negation.olean
+lib/lean/Std/Sat/CNF/Negation.olean.private
+lib/lean/Std/Sat/CNF/Negation.olean.server
+lib/lean/Std/Sat/CNF/Redundancy.ilean
+lib/lean/Std/Sat/CNF/Redundancy.ir
+lib/lean/Std/Sat/CNF/Redundancy.ir.sig
+lib/lean/Std/Sat/CNF/Redundancy.olean
+lib/lean/Std/Sat/CNF/Redundancy.olean.private
+lib/lean/Std/Sat/CNF/Redundancy.olean.server
lib/lean/Std/Sat/CNF/Relabel.ilean
lib/lean/Std/Sat/CNF/Relabel.ir
lib/lean/Std/Sat/CNF/Relabel.ir.sig
@@ -14126,6 +14150,24 @@ lib/lean/Std/Sat/CNF/RelabelFin.ir.sig
lib/lean/Std/Sat/CNF/RelabelFin.olean
lib/lean/Std/Sat/CNF/RelabelFin.olean.private
lib/lean/Std/Sat/CNF/RelabelFin.olean.server
+lib/lean/Std/Sat/CNF/Sat.ilean
+lib/lean/Std/Sat/CNF/Sat.ir
+lib/lean/Std/Sat/CNF/Sat.ir.sig
+lib/lean/Std/Sat/CNF/Sat.olean
+lib/lean/Std/Sat/CNF/Sat.olean.private
+lib/lean/Std/Sat/CNF/Sat.olean.server
+lib/lean/Std/Sat/CNF/SpecLemmas.ilean
+lib/lean/Std/Sat/CNF/SpecLemmas.ir
+lib/lean/Std/Sat/CNF/SpecLemmas.ir.sig
+lib/lean/Std/Sat/CNF/SpecLemmas.olean
+lib/lean/Std/Sat/CNF/SpecLemmas.olean.private
+lib/lean/Std/Sat/CNF/SpecLemmas.olean.server
+lib/lean/Std/Sat/CNF/Unit.ilean
+lib/lean/Std/Sat/CNF/Unit.ir
+lib/lean/Std/Sat/CNF/Unit.ir.sig
+lib/lean/Std/Sat/CNF/Unit.olean
+lib/lean/Std/Sat/CNF/Unit.olean.private
+lib/lean/Std/Sat/CNF/Unit.olean.server
lib/lean/Std/Sync.ilean
lib/lean/Std/Sync.ir
lib/lean/Std/Sync.ir.sig
@@ -14606,126 +14648,60 @@ lib/lean/Std/Tactic/BVDecide/LRAT/Checker.ir.sig
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean.private
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.olean.server
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ilean
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ir
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ir.sig
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean.private
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean.server
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ilean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ir
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ir.sig
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean.private
-lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.olean.server
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.ilean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.ir
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.ir.sig
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.olean
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.olean.private
+lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.olean.server
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ilean
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ir
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ir.sig
@@ -16335,6 +16311,7 @@ src/lean/Lean/Elab/Tactic/Repeat.lean
src/lean/Lean/Elab/Tactic/Rewrite.lean
src/lean/Lean/Elab/Tactic/Rewrites.lean
src/lean/Lean/Elab/Tactic/Rfl.lean
+src/lean/Lean/Elab/Tactic/Rwa.lean
src/lean/Lean/Elab/Tactic/Show.lean
src/lean/Lean/Elab/Tactic/ShowTerm.lean
src/lean/Lean/Elab/Tactic/Simp.lean
@@ -17397,9 +17374,15 @@ src/lean/Std/Sat/AIG/RelabelNat.lean
src/lean/Std/Sat/CNF.lean
src/lean/Std/Sat/CNF/Basic.lean
src/lean/Std/Sat/CNF/Dimacs.lean
+src/lean/Std/Sat/CNF/Entails.lean
src/lean/Std/Sat/CNF/Literal.lean
+src/lean/Std/Sat/CNF/Negation.lean
+src/lean/Std/Sat/CNF/Redundancy.lean
src/lean/Std/Sat/CNF/Relabel.lean
src/lean/Std/Sat/CNF/RelabelFin.lean
+src/lean/Std/Sat/CNF/Sat.lean
+src/lean/Std/Sat/CNF/SpecLemmas.lean
+src/lean/Std/Sat/CNF/Unit.lean
src/lean/Std/Sync.lean
src/lean/Std/Sync/Barrier.lean
src/lean/Std/Sync/Basic.lean
@@ -17480,26 +17463,15 @@ src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
src/lean/Std/Tactic/BVDecide/LRAT.lean
src/lean/Std/Tactic/BVDecide/LRAT/Actions.lean
src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Add.lean
src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATChecker.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/CompactLRATCheckerSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
-src/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Basic.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Checker.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Delete.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Empty.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Rat.lean
+src/lean/Std/Tactic/BVDecide/LRAT/Internal/Rup.lean
src/lean/Std/Tactic/BVDecide/LRAT/Parser.lean
src/lean/Std/Tactic/BVDecide/Normalize.lean
src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
diff --git a/lean4-git/distinfo b/lean4-git/distinfo
index 38f42c3b7e..71c1be06f9 100644
--- a/lean4-git/distinfo
+++ b/lean4-git/distinfo
@@ -7,7 +7,7 @@ SHA1 (patch-src_CMakeLists.txt) = c6620d0ca4c6f5d2fccf4e8e97462661c1a9d38d
SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
SHA1 (patch-src_include_lean_lean.h) = 017a9c5b5ac185a122a831f6fe4a64e94d9caad9
SHA1 (patch-src_lake_Lake_Build_Common.lean) = d629442adea33b122932170b0ed13397760716d4
-SHA1 (patch-src_runtime_process.cpp) = 1e7c52020fb047ca75816bd20a35a10c9a9f5b5b
+SHA1 (patch-src_runtime_process.cpp) = 2a064f747f0448be92e6426e1ba91e34e9d5ca60
SHA1 (patch-stage0_src_CMakeLists.txt) = 9605c8287537786cec326e6d6f041faa4ce3f1ae
SHA1 (patch-stage0_src_include_lean_lean.h) = b138c9a082107a667ee3df0623c2ab0e6b2a546f
-SHA1 (patch-stage0_src_runtime_process.cpp) = 9fc39977e845282991d790f3949597c02cf5c30b
+SHA1 (patch-stage0_src_runtime_process.cpp) = afc46a9ee553a370da3a29ba1e907c6351a5eb1c
diff --git a/lean4-git/patches/patch-src_runtime_process.cpp b/lean4-git/patches/patch-src_runtime_process.cpp
index f06898b48d..f2dd6a2589 100644
--- a/lean4-git/patches/patch-src_runtime_process.cpp
+++ b/lean4-git/patches/patch-src_runtime_process.cpp
@@ -4,9 +4,22 @@ Set proper thread id on NetBSD.
clearenv() does not exist on NetBSD.
https://github.com/leanprover/lean4/pull/14543
---- src/runtime/process.cpp.orig 2026-08-15 19:18:21.675172496 +0000
+Create environment before forking
+https://github.com/leanprover/lean4/issues/14587
+
+--- src/runtime/process.cpp.orig 2026-08-15 19:18:21.000000000 +0000
+++ src/runtime/process.cpp
-@@ -341,6 +341,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
+@@ -8,7 +8,9 @@ Author: Jared Roesch
+ #include <fstream>
+ #include <iostream>
+ #include <iomanip>
++#include <map>
+ #include <utility>
++#include <vector>
+ #include <system_error>
+
+ #if defined(LEAN_WINDOWS)
+@@ -341,6 +343,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
uint64_t tid;
#ifdef __APPLE__
lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
@@ -15,7 +28,7 @@ https://github.com/leanprover/lean4/pull/14543
#elif defined(LEAN_EMSCRIPTEN)
tid = 0;
#else
-@@ -431,7 +433,7 @@ static optional<pipe> setup_stdio(stdio cfg) {
+@@ -431,10 +435,52 @@ static optional<pipe> setup_stdio(stdio cfg) {
lean_unreachable();
}
@@ -24,12 +37,96 @@ https://github.com/leanprover/lean4/pull/14543
extern "C" char **environ;
#endif
-@@ -454,7 +456,7 @@ static obj_res spawn(string_ref const & proc_name, arr
++static std::vector<char*> build_environ(bool inherit_env, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env) {
++ std::map<std::string, std::string> current;
++ if (inherit_env) {
++ /* Build a lookup map from current environ */
++ for (char** env = environ; *env; ++env) {
++ auto sep = std::strstr(*env, "=");
++ if (sep) {
++ std::string key(*env, sep - *env);
++ current[std::move(key)] = sep + 1;
++ }
++ }
++ }
++
++ /* Apply overrides */
++ for (auto & entry : env) {
++ if (entry.snd()) {
++ current[entry.fst().data()] = entry.snd().get()->data();
++ } else {
++ current.erase(entry.fst().data());
++ }
++ }
++
++ /* Create the new environ array */
++ std::vector<char*> result;
++ result.reserve(current.size() + 1);
++
++ for (auto & [key, val] : current) {
++ size_t key_len = key.size();
++ size_t val_len = val.size();
++ size_t total = key_len + 1 + val_len + 1;
++ char* entry = new char[total];
++ std::memcpy(entry, key.data(), key_len);
++ entry[key_len] = '=';
++ std::memcpy(entry + key_len + 1, val.data(), val_len);
++ entry[key_len + 1 + val_len] = '\0';
++ result.push_back(entry);
++ }
++
++ result.push_back(nullptr);
++ return result;
++}
++
+ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const & args, stdio stdin_mode, stdio stdout_mode,
+ stdio stderr_mode, option_ref<string_ref> const & cwd, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env,
+ bool inherit_env, bool do_setsid) {
+@@ -450,24 +496,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ pargs.push_back(strdup(arg.data()));
+ pargs.push_back(NULL);
+
++ std::vector<char*> new_env = build_environ(inherit_env, env);
++
+ int pid = fork();
if (pid == 0) {
- if (!inherit_env) {
+- if (!inherit_env) {
-#ifdef __APPLE__
-+#if defined(__APPLE__) || defined(__NetBSD__)
- environ = NULL;
- #else
- clearenv();
+- environ = NULL;
+-#else
+- clearenv();
+-#endif
+- }
+- for (auto & entry : env) {
+- if (entry.snd()) {
+- setenv(entry.fst().data(), entry.snd().get()->data(), true);
+- } else {
+- unsetenv(entry.fst().data());
+- }
+- }
+-
+ if (stdin_pipe) {
+ dup2(stdin_pipe->m_read_fd, STDIN_FILENO);
+ close(stdin_pipe->m_write_fd);
+@@ -507,7 +540,7 @@ static obj_res spawn(string_ref const & proc_name, arr
+ lean_always_assert(setsid() >= 0);
+ }
+
+- if (execvp(pargs[0], pargs.data()) < 0) {
++ if (execvpe(pargs[0], pargs.data(), new_env.data()) < 0) {
+ std::cerr << "could not execute external process '" << pargs[0] << "'" << std::endl;
+ // See the comment above about `_exit` vs `exit`.
+ _exit(-1);
+@@ -520,6 +553,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ if (parg != NULL) {
+ free(parg);
+ }
++ }
++ for (char* entry : new_env) {
++ if (entry != NULL) {
++ free(entry);
++ }
+ }
+
+ object * parent_stdin = box(0);
diff --git a/lean4-git/patches/patch-stage0_src_runtime_process.cpp b/lean4-git/patches/patch-stage0_src_runtime_process.cpp
index b6c7e4b1d2..641d25c68b 100644
--- a/lean4-git/patches/patch-stage0_src_runtime_process.cpp
+++ b/lean4-git/patches/patch-stage0_src_runtime_process.cpp
@@ -4,9 +4,22 @@ Set proper thread id on NetBSD.
clearenv() does not exist on NetBSD.
https://github.com/leanprover/lean4/pull/14543
---- stage0/src/runtime/process.cpp.orig 2026-08-15 19:18:21.681242044 +0000
+Create environment before forking
+https://github.com/leanprover/lean4/issues/14587
+
+--- stage0/src/runtime/process.cpp.orig 2026-08-15 19:18:21.000000000 +0000
+++ stage0/src/runtime/process.cpp
-@@ -341,6 +341,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
+@@ -8,7 +8,9 @@ Author: Jared Roesch
+ #include <fstream>
+ #include <iostream>
+ #include <iomanip>
++#include <map>
+ #include <utility>
++#include <vector>
+ #include <system_error>
+
+ #if defined(LEAN_WINDOWS)
+@@ -341,6 +343,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
uint64_t tid;
#ifdef __APPLE__
lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
@@ -15,7 +28,7 @@ https://github.com/leanprover/lean4/pull/14543
#elif defined(LEAN_EMSCRIPTEN)
tid = 0;
#else
-@@ -431,7 +433,7 @@ static optional<pipe> setup_stdio(stdio cfg) {
+@@ -431,10 +435,52 @@ static optional<pipe> setup_stdio(stdio cfg) {
lean_unreachable();
}
@@ -24,12 +37,96 @@ https://github.com/leanprover/lean4/pull/14543
extern "C" char **environ;
#endif
-@@ -454,7 +456,7 @@ static obj_res spawn(string_ref const & proc_name, arr
++static std::vector<char*> build_environ(bool inherit_env, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env) {
++ std::map<std::string, std::string> current;
++ if (inherit_env) {
++ /* Build a lookup map from current environ */
++ for (char** env = environ; *env; ++env) {
++ auto sep = std::strstr(*env, "=");
++ if (sep) {
++ std::string key(*env, sep - *env);
++ current[std::move(key)] = sep + 1;
++ }
++ }
++ }
++
++ /* Apply overrides */
++ for (auto & entry : env) {
++ if (entry.snd()) {
++ current[entry.fst().data()] = entry.snd().get()->data();
++ } else {
++ current.erase(entry.fst().data());
++ }
++ }
++
++ /* Create the new environ array */
++ std::vector<char*> result;
++ result.reserve(current.size() + 1);
++
++ for (auto & [key, val] : current) {
++ size_t key_len = key.size();
++ size_t val_len = val.size();
++ size_t total = key_len + 1 + val_len + 1;
++ char* entry = new char[total];
++ std::memcpy(entry, key.data(), key_len);
++ entry[key_len] = '=';
++ std::memcpy(entry + key_len + 1, val.data(), val_len);
++ entry[key_len + 1 + val_len] = '\0';
++ result.push_back(entry);
++ }
++
++ result.push_back(nullptr);
++ return result;
++}
++
+ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const & args, stdio stdin_mode, stdio stdout_mode,
+ stdio stderr_mode, option_ref<string_ref> const & cwd, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env,
+ bool inherit_env, bool do_setsid) {
+@@ -450,24 +496,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ pargs.push_back(strdup(arg.data()));
+ pargs.push_back(NULL);
+
++ std::vector<char*> new_env = build_environ(inherit_env, env);
++
+ int pid = fork();
if (pid == 0) {
- if (!inherit_env) {
+- if (!inherit_env) {
-#ifdef __APPLE__
-+#if defined(__APPLE__) || defined(__NetBSD__)
- environ = NULL;
- #else
- clearenv();
+- environ = NULL;
+-#else
+- clearenv();
+-#endif
+- }
+- for (auto & entry : env) {
+- if (entry.snd()) {
+- setenv(entry.fst().data(), entry.snd().get()->data(), true);
+- } else {
+- unsetenv(entry.fst().data());
+- }
+- }
+-
+ if (stdin_pipe) {
+ dup2(stdin_pipe->m_read_fd, STDIN_FILENO);
+ close(stdin_pipe->m_write_fd);
+@@ -507,7 +540,7 @@ static obj_res spawn(string_ref const & proc_name, arr
+ lean_always_assert(setsid() >= 0);
+ }
+
+- if (execvp(pargs[0], pargs.data()) < 0) {
++ if (execvpe(pargs[0], pargs.data(), new_env.data()) < 0) {
+ std::cerr << "could not execute external process '" << pargs[0] << "'" << std::endl;
+ // See the comment above about `_exit` vs `exit`.
+ _exit(-1);
+@@ -520,6 +553,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ if (parg != NULL) {
+ free(parg);
+ }
++ }
++ for (char* entry : new_env) {
++ if (entry != NULL) {
++ free(entry);
++ }
+ }
+
+ object * parent_stdin = box(0);
Home |
Main Index |
Thread Index |
Old Index