Menu
▾
▴
hol-checkins — Check-in messages from everything done in the HOL project.
You can subscribe to this list here.
| 2001 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
(21) |
Sep
(54) |
Oct
(196) |
Nov
(158) |
Dec
(139) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2002 |
Jan
(62) |
Feb
(98) |
Mar
(42) |
Apr
(137) |
May
(141) |
Jun
(108) |
Jul
(70) |
Aug
(117) |
Sep
(106) |
Oct
(25) |
Nov
(34) |
Dec
(27) |
| 2003 |
Jan
(53) |
Feb
(53) |
Mar
(102) |
Apr
(62) |
May
(10) |
Jun
(77) |
Jul
(83) |
Aug
(72) |
Sep
(74) |
Oct
(118) |
Nov
(6) |
Dec
(6) |
| 2004 |
Jan
(89) |
Feb
(43) |
Mar
(41) |
Apr
(20) |
May
(30) |
Jun
(60) |
Jul
(204) |
Aug
(79) |
Sep
(19) |
Oct
(37) |
Nov
(25) |
Dec
(34) |
| 2005 |
Jan
(174) |
Feb
(107) |
Mar
(48) |
Apr
(70) |
May
(35) |
Jun
(115) |
Jul
(257) |
Aug
(63) |
Sep
(62) |
Oct
(51) |
Nov
(68) |
Dec
(47) |
| 2006 |
Jan
(50) |
Feb
(129) |
Mar
(73) |
Apr
(13) |
May
(91) |
Jun
(135) |
Jul
(104) |
Aug
(117) |
Sep
(151) |
Oct
(101) |
Nov
(69) |
Dec
(51) |
| 2007 |
Jan
(68) |
Feb
(45) |
Mar
(44) |
Apr
(21) |
May
(40) |
Jun
(27) |
Jul
(76) |
Aug
(29) |
Sep
(12) |
Oct
(61) |
Nov
(32) |
Dec
(16) |
| 2008 |
Jan
(35) |
Feb
(26) |
Mar
(46) |
Apr
(79) |
May
(61) |
Jun
(38) |
Jul
(58) |
Aug
(64) |
Sep
(96) |
Oct
(86) |
Nov
(66) |
Dec
(80) |
| 2009 |
Jan
(53) |
Feb
(81) |
Mar
(104) |
Apr
(68) |
May
(61) |
Jun
(78) |
Jul
(138) |
Aug
(74) |
Sep
(157) |
Oct
(132) |
Nov
(113) |
Dec
(78) |
| 2010 |
Jan
(129) |
Feb
(101) |
Mar
(146) |
Apr
(158) |
May
(85) |
Jun
(98) |
Jul
(80) |
Aug
(124) |
Sep
(123) |
Oct
(98) |
Nov
(37) |
Dec
(51) |
| 2011 |
Jan
(82) |
Feb
(36) |
Mar
(50) |
Apr
(50) |
May
(52) |
Jun
(62) |
Jul
(33) |
Aug
(61) |
Sep
(125) |
Oct
(63) |
Nov
(14) |
Dec
(17) |
| 2012 |
Jan
(22) |
Feb
(36) |
Mar
(177) |
Apr
(77) |
May
(60) |
Jun
(46) |
Jul
(127) |
Aug
(96) |
Sep
(58) |
Oct
(72) |
Nov
(40) |
Dec
(44) |
| 2013 |
Jan
(42) |
Feb
(42) |
Mar
(5) |
Apr
(24) |
May
(38) |
Jun
(25) |
Jul
(36) |
Aug
(35) |
Sep
(9) |
Oct
(29) |
Nov
(60) |
Dec
(24) |
| 2014 |
Jan
(26) |
Feb
(32) |
Mar
(28) |
Apr
(28) |
May
(35) |
Jun
(34) |
Jul
(23) |
Aug
(37) |
Sep
(28) |
Oct
(33) |
Nov
(38) |
Dec
(24) |
| 2015 |
Jan
(36) |
Feb
(38) |
Mar
(54) |
Apr
(4) |
May
(16) |
Jun
(21) |
Jul
(25) |
Aug
(65) |
Sep
(54) |
Oct
(63) |
Nov
(60) |
Dec
(35) |
| 2016 |
Jan
(106) |
Feb
(35) |
Mar
(93) |
Apr
(65) |
May
(45) |
Jun
(48) |
Jul
(44) |
Aug
(65) |
Sep
(48) |
Oct
(31) |
Nov
(63) |
Dec
(33) |
| 2017 |
Jan
(46) |
Feb
(48) |
Mar
(36) |
Apr
(38) |
May
(39) |
Jun
(65) |
Jul
(49) |
Aug
(48) |
Sep
(52) |
Oct
(86) |
Nov
(31) |
Dec
(22) |
| 2018 |
Jan
(60) |
Feb
(21) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2019 |
Jan
(29) |
Feb
(122) |
Mar
(112) |
Apr
(60) |
May
(141) |
Jun
(75) |
Jul
(83) |
Aug
(73) |
Sep
(48) |
Oct
(67) |
Nov
(124) |
Dec
(34) |
| 2020 |
Jan
(115) |
Feb
(138) |
Mar
(63) |
Apr
(26) |
May
(102) |
Jun
(85) |
Jul
(51) |
Aug
(106) |
Sep
(44) |
Oct
(43) |
Nov
(40) |
Dec
(82) |
| 2021 |
Jan
(75) |
Feb
(35) |
Mar
(65) |
Apr
(11) |
May
(79) |
Jun
(48) |
Jul
(41) |
Aug
(66) |
Sep
(45) |
Oct
(55) |
Nov
(88) |
Dec
(50) |
| 2022 |
Jan
(67) |
Feb
(51) |
Mar
(43) |
Apr
(37) |
May
(26) |
Jun
(25) |
Jul
(16) |
Aug
(26) |
Sep
(24) |
Oct
(24) |
Nov
(16) |
Dec
(23) |
| 2023 |
Jan
(32) |
Feb
(8) |
Mar
(6) |
Apr
(6) |
May
(22) |
Jun
(42) |
Jul
(52) |
Aug
(45) |
Sep
(29) |
Oct
(30) |
Nov
(40) |
Dec
(24) |
| 2024 |
Jan
(67) |
Feb
(40) |
Mar
(33) |
Apr
(47) |
May
(50) |
Jun
(46) |
Jul
(41) |
Aug
(41) |
Sep
(33) |
Oct
(70) |
Nov
(53) |
Dec
(103) |
| 2025 |
Jan
(40) |
Feb
(58) |
Mar
(86) |
Apr
(110) |
May
(104) |
Jun
(85) |
Jul
(130) |
Aug
(86) |
Sep
(61) |
Oct
(95) |
Nov
(27) |
Dec
(31) |
| 2026 |
Jan
(195) |
Feb
(137) |
Mar
(286) |
Apr
(156) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: Ramana K. <no...@gi...> - 2026-04-28 11:47:36
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 71e4d5bbe8da49ac63c33cecffa72bfc5a69907e https://github.com/HOL-Theorem-Prover/HOL/commit/71e4d5bbe8da49ac63c33cecffa72bfc5a69907e Author: Ramana Kumar <ra...@me...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTEmit.sml M src/postkernel/prooftrace/pft-ruleset-candle.md Log Message: ----------- Require NUMERAL wrapping in Candle compute expressions To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-28 06:17:34
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 089b98e5a814e9c11ef656404d768af2c1eb9c16 https://github.com/HOL-Theorem-Prover/HOL/commit/089b98e5a814e9c11ef656404d768af2c1eb9c16 Author: Ramana Kumar <ra...@me...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml M src/postkernel/prooftrace/PFTEmit.sml Log Message: ----------- Use cval type properly To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Michael N. <no...@gi...> - 2026-04-28 00:47:08
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/hol-webpages Commit: d67516d5b9150f96b688a60eee2c2034d0797f1b https://github.com/HOL-Theorem-Prover/hol-webpages/commit/d67516d5b9150f96b688a60eee2c2034d0797f1b Author: Michael Norrish <mic...@an...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M new-look/index.html Log Message: ----------- Minor languge tweaks in installation section To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/hol-webpages/settings/notifications |
|
From: Michael N. <no...@gi...> - 2026-04-28 00:42:08
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/hol-webpages Commit: ed3e33060cdd7dfaf58302c46c09c77e896bebfa https://github.com/HOL-Theorem-Prover/hol-webpages/commit/ed3e33060cdd7dfaf58302c46c09c77e896bebfa Author: Michael Norrish <mic...@an...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M new-look/index.html Log Message: ----------- Tweak ul of last commit To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/hol-webpages/settings/notifications |
|
From: Shrys <no...@gi...> - 2026-04-28 00:29:02
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/hol-webpages Commit: aa59697a940292687c4698e5e1d13ad29ed2e5c8 https://github.com/HOL-Theorem-Prover/hol-webpages/commit/aa59697a940292687c4698e5e1d13ad29ed2e5c8 Author: Shreyas <shr...@gm...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M new-look/index.html Log Message: ----------- Initial attempt To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/hol-webpages/settings/notifications |
|
From: Chun T. <no...@gi...> - 2026-04-27 23:52:12
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 2bc77711c2c1d20a66daa7209b81f1d2e4ebe75a https://github.com/HOL-Theorem-Prover/HOL/commit/2bc77711c2c1d20a66daa7209b81f1d2e4ebe75a Author: Chun Tian (binghe) <bin...@gm...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M examples/lambda/barendregt/boehmScript.sml M examples/lambda/barendregt/chap2Script.sml M examples/lambda/barendregt/chap3Script.sml M examples/lambda/barendregt/head_reductionScript.sml M examples/lambda/barendregt/solvableScript.sml M examples/lambda/barendregt/takahashiS3Script.sml Log Message: ----------- Some lemmas about eta-reduction and beta-eta equivalence Commit: 059423e54b150d42f36309bb70ed789e9619e560 https://github.com/HOL-Theorem-Prover/HOL/commit/059423e54b150d42f36309bb70ed789e9619e560 Author: Chun Tian (binghe) <bin...@gm...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M examples/lambda/barendregt/chap3Script.sml M examples/lambda/barendregt/head_reductionScript.sml M examples/lambda/barendregt/horeductionScript.sml M examples/lambda/barendregt/solvableScript.sml Log Message: ----------- Use Overload syntax; add further hnf_bestar_cases Commit: 49d055302c1a002be77ab39b156e838c525b2401 https://github.com/HOL-Theorem-Prover/HOL/commit/49d055302c1a002be77ab39b156e838c525b2401 Author: Chun Tian (binghe) <bin...@gm...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M examples/lambda/barendregt/boehmScript.sml Log Message: ----------- Fix statements of lameq_subterm_cong Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/e519ff8310f7...49d055302c1a To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-27 23:51:22
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: e519ff8310f78fbfcd21ece3a05473dc9ae87974 https://github.com/HOL-Theorem-Prover/HOL/commit/e519ff8310f78fbfcd21ece3a05473dc9ae87974 Author: Ramana Kumar <ra...@me...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M src/postkernel/prooftrace/.gitignore M src/postkernel/prooftrace/Holmakefile A src/postkernel/prooftrace/PFTOpcodes.sig A src/postkernel/prooftrace/PFTOpcodes.sml A src/postkernel/prooftrace/PFTReader.sig A src/postkernel/prooftrace/PFTReader.sml A src/postkernel/prooftrace/PFTReplay.sig A src/postkernel/prooftrace/PFTReplay.sml A src/postkernel/prooftrace/pft-format.md A src/postkernel/prooftrace/pft-replay-test.mlb A src/postkernel/prooftrace/pft-replay-test.sml A src/postkernel/prooftrace/pft-replay.mlb A src/postkernel/prooftrace/pft-ruleset-hol4.md Log Message: ----------- Add PFT replay module This commit introduces the PFT format for HOL proof traces and a standalone tool for replaying proofs in that format in HOL4. In the future we intend to also integrate such replay in the system using the --thmsrc option of Holmake/build. To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Matt <no...@gi...> - 2026-04-27 23:50:05
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 7f7569b2ff73df7ae51c45658ec889ef8448bd08 https://github.com/HOL-Theorem-Prover/HOL/commit/7f7569b2ff73df7ae51c45658ec889ef8448bd08 Author: Matt <328...@us...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: A src/basicProof/theory_tests/suspNestedScript.sml M src/marker/markerLib.sig M src/marker/markerLib.sml M src/marker/selftest.sml Log Message: ----------- Fix nested suspense/resume proofs (#1923) * fix nested suspense/resume proofs * fix spacing To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-27 23:46:53
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 3de8caf0248f867d2617826b65c9c5970ed2ae3c https://github.com/HOL-Theorem-Prover/HOL/commit/3de8caf0248f867d2617826b65c9c5970ed2ae3c Author: Ramana Kumar <ra...@me...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M tools-poly/lsp-server.ML Log Message: ----------- Add HOL parse trees to LSP server Work on #1846 Commit: 7bc6aec42d6565d6aad32fc911d50bda9b872d4f https://github.com/HOL-Theorem-Prover/HOL/commit/7bc6aec42d6565d6aad32fc911d50bda9b872d4f Author: Ramana Kumar <ra...@me...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M tools-poly/holide.ML M tools-poly/lsp-server.ML Log Message: ----------- Switch to built trees instead of hol/ml trees Commit: 5f6f73f0c886ce558a2822325c1254de786ddc0f https://github.com/HOL-Theorem-Prover/HOL/commit/5f6f73f0c886ce558a2822325c1254de786ddc0f Author: Ramana Kumar <ra...@me...> Date: 2026-04-28 (Tue, 28 Apr 2026) Changed paths: M tools-poly/holide.ML M tools-poly/lsp-server.ML Log Message: ----------- Don't change the navigation logic so much Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/1d7b982dc38e...5f6f73f0c886 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-27 15:48:58
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 9d13a9ff7feefd73e132ffef8586cccfd7d3ad2e https://github.com/HOL-Theorem-Prover/HOL/commit/9d13a9ff7feefd73e132ffef8586cccfd7d3ad2e Author: Ramana Kumar <ra...@me...> Date: 2026-04-27 (Mon, 27 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Try to fix more compute preamble bugs To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-27 13:45:52
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 81d9c383e0c63127e2b888ff32c57985ce5f7623 https://github.com/HOL-Theorem-Prover/HOL/commit/81d9c383e0c63127e2b888ff32c57985ce5f7623 Author: Ramana Kumar <ra...@me...> Date: 2026-04-27 (Mon, 27 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Fix some bugs (and misleading comments) To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-27 12:58:19
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 7e9d3dca728b66acf34dbfd21619f7c7ca2d9744 https://github.com/HOL-Theorem-Prover/HOL/commit/7e9d3dca728b66acf34dbfd21619f7c7ca2d9744 Author: Ramana Kumar <ra...@me...> Date: 2026-04-27 (Mon, 27 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Fix variable names in compute preamble To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-27 11:36:00
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 1621a1582a656718c45c8b49c943595e34931422 https://github.com/HOL-Theorem-Prover/HOL/commit/1621a1582a656718c45c8b49c943595e34931422 Author: Ramana Kumar <ra...@me...> Date: 2026-04-27 (Mon, 27 Apr 2026) Changed paths: M src/postkernel/prooftrace/pft-ruleset-candle.md Log Message: ----------- Clarify types for COND equations To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-27 11:28:28
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 9ac2d62500b252e9d451398ae206bd33678d7744 https://github.com/HOL-Theorem-Prover/HOL/commit/9ac2d62500b252e9d451398ae206bd33678d7744 Author: Ramana Kumar <ra...@me...> Date: 2026-04-27 (Mon, 27 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Delete some dead code Commit: 0660ae8c158ce4a22a3ad9ea97d16bcc75cb4597 https://github.com/HOL-Theorem-Prover/HOL/commit/0660ae8c158ce4a22a3ad9ea97d16bcc75cb4597 Author: Ramana Kumar <ra...@me...> Date: 2026-04-27 (Mon, 27 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sig M src/postkernel/prooftrace/PFTCandleComputePreamble.sml M src/postkernel/prooftrace/pft-ruleset-candle.md Log Message: ----------- Try to fix candle compute equations Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/add0ce133570...0660ae8c158c To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-26 08:20:59
|
Branch: refs/heads/pftreplay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 9d222488d57c605bf7ada9f96632760f660ce051 https://github.com/HOL-Theorem-Prover/HOL/commit/9d222488d57c605bf7ada9f96632760f660ce051 Author: Ramana Kumar <ra...@me...> Date: 2026-04-26 (Sun, 26 Apr 2026) Changed paths: M src/postkernel/prooftrace/.gitignore M src/postkernel/prooftrace/Holmakefile A src/postkernel/prooftrace/PFTOpcodes.sig A src/postkernel/prooftrace/PFTOpcodes.sml A src/postkernel/prooftrace/PFTReader.sig A src/postkernel/prooftrace/PFTReader.sml A src/postkernel/prooftrace/PFTReplay.sig A src/postkernel/prooftrace/PFTReplay.sml A src/postkernel/prooftrace/pft-format.md A src/postkernel/prooftrace/pft-replay-test.mlb A src/postkernel/prooftrace/pft-replay-test.sml A src/postkernel/prooftrace/pft-replay.mlb A src/postkernel/prooftrace/pft-ruleset-hol4.md Log Message: ----------- Add PFT replay module This commit introduces the PFT format for HOL proof traces and a standalone tool for replaying proofs in that format in HOL4. In the future we intend to also integrate such replay in the system using the --thmsrc option of Holmake/build. To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Konrad S. <no...@gi...> - 2026-04-25 04:38:29
|
Branch: refs/heads/nfa-develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: a53e7f7d4e90dc4146ca722eb5e1d2b98afebfb8 https://github.com/HOL-Theorem-Prover/HOL/commit/a53e7f7d4e90dc4146ca722eb5e1d2b98afebfb8 Author: Konrad Slind <kon...@gm...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: A examples/formal-languages/regular/tutorial/tutorialScript.sml R examples/formal-languages/regular/tutorialScript.sml Log Message: ----------- start tutorial Commit: 8343f3fa0c2473573b0fea6283d65f00976567b1 https://github.com/HOL-Theorem-Prover/HOL/commit/8343f3fa0c2473573b0fea6283d65f00976567b1 Author: Konrad Slind <kon...@gm...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: A examples/formal-languages/regular/automata-tutorial/.gitignore A examples/formal-languages/regular/automata-tutorial/book.toml A examples/formal-languages/regular/automata-tutorial/src/README.md A examples/formal-languages/regular/automata-tutorial/src/Summary.md A examples/formal-languages/regular/automata-tutorial/src/definitions.md A examples/formal-languages/regular/automata-tutorial/src/dfa-to-nfa.md A examples/formal-languages/regular/automata-tutorial/src/final-result.md A examples/formal-languages/regular/automata-tutorial/src/nfa-to-dfa.md Log Message: ----------- start tutorial in mdbook Commit: 38de2b803355e471bce93e260618a49f6b3e2dd9 https://github.com/HOL-Theorem-Prover/HOL/commit/38de2b803355e471bce93e260618a49f6b3e2dd9 Author: Konrad Slind <kon...@gm...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: A examples/formal-languages/regular/automata-tutorial/tutorialScript.sml R examples/formal-languages/regular/tutorial/tutorialScript.sml Log Message: ----------- moving tutorialScript.sml about the place Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/dfeaf8ac4cd0...38de2b803355 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-24 23:39:43
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 89a03a3eb4fa277db147202128ce92043559f9fc https://github.com/HOL-Theorem-Prover/HOL/commit/89a03a3eb4fa277db147202128ce92043559f9fc Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sig Log Message: ----------- Add fixed input theorems for PFTCandleComputePreamble The derivations need to be updated still Commit: 76dddfe116461fe2ddcfe75be08292a6c49de4de https://github.com/HOL-Theorem-Prover/HOL/commit/76dddfe116461fe2ddcfe75be08292a6c49de4de Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Update derivation for BIT1 Commit: b105abd9accac3ab228e5e4e6ec7ce75251a8f50 https://github.com/HOL-Theorem-Prover/HOL/commit/b105abd9accac3ab228e5e4e6ec7ce75251a8f50 Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Update implementation for new inputs Commit: 8693b0b80e4586b58bd2d84eae5253dc41232c14 https://github.com/HOL-Theorem-Prover/HOL/commit/8693b0b80e4586b58bd2d84eae5253dc41232c14 Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Fix some bugs Commit: add0ce13357021d808e3a675061898af188cd82a https://github.com/HOL-Theorem-Prover/HOL/commit/add0ce13357021d808e3a675061898af188cd82a Author: Ramana Kumar <ra...@me...> Date: 2026-04-25 (Sat, 25 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Fix forall type Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/b151ac7ac1ad...add0ce133570 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-24 23:34:43
|
Branch: refs/heads/lspnew Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 6cf2c95a3068531587b80835a9546c11c4112ab2 https://github.com/HOL-Theorem-Prover/HOL/commit/6cf2c95a3068531587b80835a9546c11c4112ab2 Author: Ramana Kumar <ra...@me...> Date: 2026-04-25 (Sat, 25 Apr 2026) Changed paths: M tools-poly/holide.ML M tools-poly/lsp-server.ML Log Message: ----------- Don't change the navigation logic so much To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Konrad S. <no...@gi...> - 2026-04-24 19:51:19
|
Branch: refs/heads/nfa-develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 329b15440b99657d635b70198e1af0000bfaf832 https://github.com/HOL-Theorem-Prover/HOL/commit/329b15440b99657d635b70198e1af0000bfaf832 Author: Konrad Slind <kon...@gm...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: M examples/formal-languages/regular/nfaScript.sml Log Message: ----------- minor sprucing up Commit: dfeaf8ac4cd0cdb03df3fde2e236955ef325455e https://github.com/HOL-Theorem-Prover/HOL/commit/dfeaf8ac4cd0cdb03df3fde2e236955ef325455e Author: Konrad Slind <kon...@gm...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: A examples/formal-languages/regular/tutorialScript.sml Log Message: ----------- start on tutorial Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/d07c17432171...dfeaf8ac4cd0 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Michael N. <no...@gi...> - 2026-04-24 07:17:12
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 1d7b982dc38e4986eb817c46dafd24f8e59a35b0 https://github.com/HOL-Theorem-Prover/HOL/commit/1d7b982dc38e4986eb817c46dafd24f8e59a35b0 Author: Michael Norrish <mic...@an...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: M tools/Holmake/tests/longcmdlock/selftest.sml Log Message: ----------- Get longcmdlock selftest to pass under Moscow ML To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Michael N. <no...@gi...> - 2026-04-24 01:01:05
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: f439019142c52b17db2b9f2a60bc0d548462e707 https://github.com/HOL-Theorem-Prover/HOL/commit/f439019142c52b17db2b9f2a60bc0d548462e707 Author: Michael Norrish <mic...@an...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: M tools/Holmake/tests/parallel_tests/Holmakefile Log Message: ----------- Include new longcmdlock selftest for Holmake in std. sequence To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-24 00:56:14
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 86a5d9bc27d3d7e07299dd3cf69d4e7bebf4d5f2 https://github.com/HOL-Theorem-Prover/HOL/commit/86a5d9bc27d3d7e07299dd3cf69d4e7bebf4d5f2 Author: Ramana Kumar <ra...@me...> Date: 2026-04-24 (Fri, 24 Apr 2026) Changed paths: M tools/Holmake/core/HM_GraphBuildJ1.sml M tools/Holmake/poly/multibuild.sml A tools/Holmake/tests/longcmdlock/Holmakefile A tools/Holmake/tests/longcmdlock/selftest.sml Log Message: ----------- Don't use long command filename for locks (#1921) Fixes #1920 Includes selftest To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-23 14:57:18
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 398ef64b33b43b9534a5fe0fec569c59684bef7e https://github.com/HOL-Theorem-Prover/HOL/commit/398ef64b33b43b9534a5fe0fec569c59684bef7e Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/pipeline-test.sml Log Message: ----------- Expand hol4 pipeline test Commit: 7393be138f8dc50a9bfbdaed17f17f65848d0426 https://github.com/HOL-Theorem-Prover/HOL/commit/7393be138f8dc50a9bfbdaed17f17f65848d0426 Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sig Log Message: ----------- Document assumptions of PFTCandleComputePreamble Commit: ae0affce259369d504d9877cbc30421b8d713b4d https://github.com/HOL-Theorem-Prover/HOL/commit/ae0affce259369d504d9877cbc30421b8d713b4d Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sig M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Add do_SPEC helper to PFTCandleComputePreamble Commit: b151ac7ac1ad01e4daaf661919effa56887f1d48 https://github.com/HOL-Theorem-Prover/HOL/commit/b151ac7ac1ad01e4daaf661919effa56887f1d48 Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTCandleComputePreamble.sig M src/postkernel/prooftrace/PFTCandleComputePreamble.sml Log Message: ----------- Start fixing PFTCandleComputePreamble input thms Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/7af9a99b0580...b151ac7ac1ad To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-23 12:16:27
|
Branch: refs/heads/concurrency Home: https://github.com/HOL-Theorem-Prover/HOL Commit: a26bf56e6455ac178c287ddef932eff34fcb64d0 https://github.com/HOL-Theorem-Prover/HOL/commit/a26bf56e6455ac178c287ddef932eff34fcb64d0 Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M tools/Holmake/core/HM_GraphBuildJ1.sml M tools/Holmake/poly/multibuild.sml A tools/Holmake/tests/longcmdlock/Holmakefile A tools/Holmake/tests/longcmdlock/selftest.sml Log Message: ----------- Don't use long command filename for locks Fixes #1920 Includes selftest To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
|
From: Ramana K. <no...@gi...> - 2026-04-22 23:58:00
|
Branch: refs/heads/replay Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 7b5de00e22cd955ff810a09224487258e633f198 https://github.com/HOL-Theorem-Prover/HOL/commit/7b5de00e22cd955ff810a09224487258e633f198 Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTMerge.sml Log Message: ----------- Fix another minor bug? Commit: 7af9a99b0580629817cf77978762c413cfa6fd42 https://github.com/HOL-Theorem-Prover/HOL/commit/7af9a99b0580629817cf77978762c413cfa6fd42 Author: Ramana Kumar <ra...@me...> Date: 2026-04-23 (Thu, 23 Apr 2026) Changed paths: M src/postkernel/prooftrace/PFTEmit.sml Log Message: ----------- Fix bug with compute_preamble_emitted persistence Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/8c1c912b33b9...7af9a99b0580 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
32 messages has been excluded from this view by a project administrator.
