Skip to content

Commit

Permalink
add useful wbisim principle up to finite taus
Browse files Browse the repository at this point in the history 
commit 2d2cddffe3dfeee7bc31b0fb499fb32cd2218dd2
Author: Chun Tian (binghe) <[email protected]>
Date:   Mon Jun 3 10:42:43 2024 +1000

    Updated CCS example

commit f037e2c003269ba2d30ec185263b21be93d09a6b
Author: Chun Tian (binghe) <[email protected]>
Date:   Thu Jun 6 16:29:23 2024 +1000

    Move simple_assert to Lib

commit 0c39a0cfc34249e1315e8a75b399d6ca52892e96
Author: Chun Tian (binghe) <[email protected]>
Date:   Thu Jun 6 11:09:55 2024 +1000

    Further cleanup of hurdUtils (assert -> simple_assert)

commit a1037385a92acdb9b8bb1f0c243fe6f1f6120eaf
Author: Michael Norrish <[email protected]>
Date:   Mon Jun 3 10:48:36 2024 +1000

    Fix examples/vector given changes in 562bb668f092d

commit 1253e33fc97a9b4a28a55fc8b924787228823128
Author: Michael Norrish <[email protected]>
Date:   Fri May 31 14:16:11 2024 +1000

    Use correct Hungarian accent in Kőnig Lemma comment

    My googling suggests that oe is an acceptable ASCII-only rendering of
    this so keeping the theorem names as koenig_lemma etc is reasonable.

commit b9b2a68456b383cd20d3274ce454e41d3aded764
Author: Michael Norrish <[email protected]>
Date:   Thu May 30 15:43:26 2024 +1000

    Expose the resolution "primitive" behind resolve_then

    resolve_then requires the output of the resolution to be passed to a
    theorem-tactic (and will backtrack if the theorem-tactic fails with a HOL_ERR);
    the new gen_resolve_then will pass to any consumer/continuation, backtracking
    if *that* fails with a HOL_ERR.  The old resolve_then is then an easy
    instance of the new function.

commit 495e1a75b0754cb446be4f541f74a97793d5e01f
Author: someplaceguy <[email protected]>
Date:   Thu May 30 17:25:08 2024 +0000

    HolSmt: initial support for the exponential function

    This initial support is very limited and only consists in adding a
    couple of useful theorems to the proving context.

    Hopefully, in the future more extensive support is implemented by
    adding support for Z3's native power operator, which should allow
    HolSmt to prove a lot more goals. This implementation would need to be
    similar to the implementation of integer division, since it doesn't
    exactly match HOL4's exponential functions.

    The latter would also have a couple of limitations, namely:

    1. it would only work for Z3, since this operator is a Z3 extension
    and not part of the SMT-LIB standard
    2. proof reconstruction would not work

commit 616c94b7ddcd2adfbad79343318f43b00bc43420
Author: someplaceguy <[email protected]>
Date:   Thu May 30 11:49:17 2024 +0000

    HolSmt: add z3_tac and z3o_tac tactics

    These accept a list of theorems, like `metis_tac`. The free vars in the theorems
    are automatically quantified with `Drule.GEN_ALL` and added to the list of
    assumptions in the goal, prior to sending the goal to the SMT solver.

    This is needed to avoid any passed-in theorems to be specialized to free vars in
    the goal that happen to have the same name, which is almost always not what the
    user wants (and if the user really wants it, they can always assume such
    theorems manually if needed). This matches the behavior of `metis_tac`, thus
    avoiding unwanted surprises.

commit 074d16fdb751d549474ba38d6fdc5ec6459d4107
Author: someplaceguy <[email protected]>
Date:   Thu May 30 11:43:16 2024 +0000

    HolSmt: allow SMT solvers to peek under abbreviations

    Otherwise, they won't be able to see what the variables are being abbreviated
    to. This problem would cause some goals that can be solved with metis_tac[] to
    fail with HolSmt.

    The fix is to add the definition of the `Abbrev` symbol to the list of theorems
    that are added to the assumptions prior to calling the SMT solver.

commit fe6fe549423e55e2832f56e083e7e12bc2edc37a
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri May 24 20:26:11 2024 +1000

    FTBFS

commit 596437ee577524ec54ad041b4ac2ee03b32bd3ca
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri May 24 20:12:20 2024 +1000

    Fix Holmakefiles after moving iterateScript.sml out of src/real

commit 562bb668f092de2446cc7ac63774abefecb9be8a
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri May 24 20:10:03 2024 +1000

    Move out real-related theorems from iterateTheory

commit 77d5e30d24ada01dbe89b0cdb1e2ef170111af99
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue May 21 18:47:26 2024 +1000

    [ringLib] RING_TAC|RULE ported from HOL-Light

commit 7dc35fb6ea2e1a0b06e8a6cae7874529bcb913ed
Author: Michael Norrish <[email protected]>
Date:   Fri May 24 17:05:27 2024 +1000

    Git-ignore generated HTML in examples/generic_finite_graphs

commit 1388e15fb1088eeef73064dd5214abd047a6e9c5
Author: Michael Norrish <[email protected]>
Date:   Fri May 24 17:04:38 2024 +1000

    Remove unused entrypoints from hurdUtils; replace Cond with impl_tac

commit 19857c9570c4db45bb6410a1ced45b9ab7bb4cb7
Author: Chun Tian (binghe) <[email protected]>
Date:   Wed May 22 13:13:19 2024 +1000

    Fixed intLib to avoid noisy output; some cleanups in hurdUtils

commit afa5534d968a4985a916a525e82f5ca0a8e96c26
Author: Michael Norrish <[email protected]>
Date:   Wed May 22 20:29:43 2024 +1000

    Fix parsing issues with src/ring/src/EVAL_*

    These theories now get sucked into more theories because
    integerRingLib is also used more often.

commit 8ccf8cf879f247fc664e907ade75d02f0f3ff681
Author: Johannes Åman Pohjola <[email protected]>
Date:   Wed May 22 11:57:31 2024 +1000

    Modernise syntax for Turing machine example

commit f6c3ef26dd757ab1e390c66ca90d4018a1405d79
Author: Chun Tian <[email protected]>
Date:   Tue May 21 16:45:32 2024 +1000

    HOL-Light's INTEGER_TAC (#1238)

    * HOL-Light's INTEGER_TAC

    * Fix manual builds (by loading intLib earlier)

    * Fix trailing whitespaces...

    * Add some basic documentation about intLib.INTEGER_TAC|RULE

    * Fixed a bug in DISJ_ACI_RULE due to differences of UNDISCH between HOL4 and HOL-Light; fixed typo in next-release.md

commit fe0e72dc46aa5ca62a9ec826c69bd7dfe8dc301d
Author: Michael Norrish <[email protected]>
Date:   Thu May 16 17:08:33 2024 +1000

    Define simultaneous substitution for lambda/basics/cterm

    Not all of term's theorems about its analogue have been ported across yet.

commit c0974a790185ad6c0ab57589d4da0a7ddf2aa67e
Author: Michael Norrish <[email protected]>
Date:   Thu May 16 14:52:16 2024 +1000

    Automatically simplify numeral subtractions in ℝ

    Again, thanks to Eric Hall for the suggestion.

commit 7cbe9f6db6d94b75561563e89ba2985496b58daf
Author: Michael Norrish <[email protected]>
Date:   Thu May 16 14:24:32 2024 +1000

    Make M-h M's output prettier with new Hol_pp.print_DBselection

    Previously, the emacs mode command just made a call to the DB
    function, which emitted a list of public_data values, which didn't
    appear as nicely as the output from M-h f.

    Thanks to Eric Hall for the suggestion.

commit f0bc0d88e61776435fda60535bbb7d27f475bfc6
Author: Michael Norrish <[email protected]>
Date:   Wed May 15 16:49:38 2024 +1000

    Document mapPartial in DESCRIPTION

commit fbdc2552a0d2d017c021f461d1a4600bd44bc8fd
Author: Michael Norrish <[email protected]>
Date:   Wed May 15 16:49:14 2024 +1000

    Minor tweaks to DESCRIPTION's section on lists

commit 24748e92c45d14387b97d38746721d4a47f91694
Author: Michael Norrish <[email protected]>
Date:   Wed May 15 15:09:58 2024 +1000

    Define a mapPartial function in listTheory

commit 38e543944dad6edf694219b16ea73b307e36c28a
Author: Michael Norrish <[email protected]>
Date:   Tue May 14 16:39:33 2024 +1000

    Get src/combin seltest to build with Holmake's tee command

commit f0ad49c15e3e3b22db36c627016eb3710d88a236
Author: Michael Norrish <[email protected]>
Date:   Tue May 14 16:38:46 2024 +1000

    [Holmake] Modify built-in tee to not create file if command fails

commit 013b19590936441fbf63bcfc835c820d9692303b
Author: Michael Norrish <[email protected]>
Date:   Tue May 14 15:45:41 2024 +1000

    Create an INCLUDES line for Keccak example

commit e780a0d412ea8ee8b61aec367e5481fe01d5d5f5
Author: Chun Tian <[email protected]>
Date:   Tue May 14 14:53:48 2024 +1000

    Combined group and ring theories from examples/algebra to core library (#1235)

    * Move combined groupTheory and ringTheory to core library; HOL-Light compatible ringLibTheory

    * Fixed missing signature of TRANS_TAC; added ANTS_TAC ported from HOL-Light

    * FTBFS examples/algebra

    * Move ANTS_TAC from Tactic to liteLib (= impl_tac); fix builds of examples/algebra/ring

commit 7f59049385c2a9152ae0477e99956d793742ef15
Author: rsoeldner <[email protected]>
Date:   Mon May 13 19:36:01 2024 +0200

    add lowercase rewrite tactics

commit 63d7fac140bb3dfbe3b7552e64a6d1ca5b522101
Author: Michael Norrish <[email protected]>
Date:   Tue May 14 14:44:54 2024 +1000

    Get examples/Crypto/Keccak to build at selftest level 1

commit 7e24888d5914a492e9ff7eb44381247e9a33dc25
Author: Michael Norrish <[email protected]>
Date:   Tue May 14 14:39:34 2024 +1000

    Delete redundant constant transfer$FUN_REL

    Use instead quotient$===>, which just needed to be made slightly more
    polymorphic. That additional polymorphism didn't break anything.

commit b4a42012d90c2666475d53dc7a083125940738fc
Author: rsoeldner <[email protected]>
Date:   Fri May 10 10:12:31 2024 +0200

    add mk_bool

commit 6862df4f5a490c21c4ca3515bcc4977d0c98856b
Author: Michael Norrish <[email protected]>
Date:   Sat May 11 11:42:08 2024 +1000

    Fix a broken INCLUDES line

commit c612b6bbc55f0e00e60779dfade8d4eb908c56bc
Author: Magnus Myreen <[email protected]>
Date:   Thu May 9 21:03:48 2024 +0200

    Get Keccak to evaluate using cv_eval

commit 142901f307ecb262f3dfa8ae7cae064c855f5efe
Author: Magnus Myreen <[email protected]>
Date:   Thu May 9 10:00:19 2024 +0200

    Get Keccak_{256,224} and SHA3_* functions translated

commit 041ae75108845fd94f1ac462a3d46ed09d388524
Author: Ramana Kumar <[email protected]>
Date:   Mon May 6 07:30:40 2024 +0100

    Prove cheat about LOG2

commit 944e7d0381b6e14d7c74bc553071191ad5c24916
Author: Ramana Kumar <[email protected]>
Date:   Sun May 5 23:29:12 2024 +0100

    Add bool_lookup_def to the compset

commit 0c7ee73248eaf2a0725e4e4ce47559decf1ccf6e
Author: Ramana Kumar <[email protected]>
Date:   Sun May 5 23:28:50 2024 +0100

    Add prefer_num() to avoid incorrect number parsing

commit 0bd44a52fa41928e1e3c9dc7e8d3d172a2bcd9f4
Author: Ramana Kumar <[email protected]>
Date:   Sun May 5 23:28:20 2024 +0100

    Remove THE (lookup ...) and to_bool_lookup

commit af3529cf316e34a41fe0608a3f3e463276b7ec12
Author: Ramana Kumar <[email protected]>
Date:   Sun May 5 22:50:36 2024 +0100

    Remove THE (lookup ...) from theta_spt_def

commit c2b26fa2972e7d86cbd97ac29f501b9499b6bff4
Author: Magnus Myreen <[email protected]>
Date:   Fri May 3 00:27:19 2024 +0200

    Translate most of Keccak functions (with a few cheats)

commit 5730d611644cd504bd6c3af20b0e1412ada9bd8f
Author: Magnus Myreen <[email protected]>
Date:   Thu May 2 19:16:29 2024 +0200

    Translate toSortedAList

commit a83ea7e32ce04efb928f38d1084c223f6333e272
Author: Michael Norrish <[email protected]>
Date:   Fri May 10 17:16:24 2024 +1000

    Fix another developers manual typo

commit fd7ceb496620624800d6f5599ae1fc121999b777
Author: Michael Norrish <[email protected]>
Date:   Fri May 10 17:12:33 2024 +1000

    Set compile-command Local-var for emacs builds of developer manual

commit a3167c8a098b10ea5fc79c2407030ecc293e424a
Author: Michael Norrish <[email protected]>
Date:   Fri May 10 17:12:02 2024 +1000

    Explain quote-filter is built-in with Poly/ML (not separate process)

commit c873050eeced0f704c51a9a87ffb422bcae94dff
Author: Michael Norrish <[email protected]>
Date:   Fri May 10 17:11:33 2024 +1000

    Correct typos in Developers manual

commit 46b102fc1653ea99e29d25979166e427a7e0a3ea
Author: Michael Norrish <[email protected]>
Date:   Fri May 10 17:11:11 2024 +1000

    Describe how build cleanall may be necessary when rebuilding

commit bbad3fd57b603a1a4d079d738e45e97d5a71e834
Author: Michael Norrish <[email protected]>
Date:   Fri May 10 17:10:52 2024 +1000

    Document upto-parallel sequence file

commit d80a6972e7f87e6f44a3e978b7c4ca972a428c76
Author: Hrutvik Kanabar <[email protected]>
Date:   Wed May 8 10:00:43 2024 +0100

    Move "print length" into `Globals`

    As per request from @mn200

commit 320e6790ea099f54ba74ea3c1b61460be75f5a97
Author: Hrutvik Kanabar <[email protected]>
Date:   Tue May 7 14:44:53 2024 +0100

    Use "print lengths" in `monadsyntax`

    As suggested by @binghe

commit e70c86e063a1a623ae5ed60554618a4d683bad48
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri May 3 15:45:55 2024 +0100

    Make `monadsyntax` more aware of print depth

commit 07e09c5cb5582ed81b05a3fe75181c595fff4e39
Merge: 325162975 4b7d02179
Author: Michael Norrish <[email protected]>
Date:   Fri May 10 10:22:29 2024 +1000

    Merge pull request #1224 from binghe/monoidTheory

    Monoid theory moved from examples/algebra to src/algebra (core library)

commit 325162975c2778e5b1bc07c199b6f1f79b9304ae
Author: Michael Norrish <[email protected]>
Date:   Mon May 6 12:45:07 2024 +1000

    Fix bad reference to bootstrap example in parallel Holmakefile

commit 6ef46c0a89323ec39ff2c2ec148d0034bbbd8d9f
Author: Michael Norrish <[email protected]>
Date:   Mon May 6 12:39:56 2024 +1000

    Fix Holmakefile bug causing unnecessary rebuilds

    By pointing the INCLUDES back at the already built
    src/num/theories/cv_compute, the files there get rebuilt (because of the
    implicit dependency on hol.state which will indeed be fresher). Then
    numheap and lots else gets rebuilt in turn.

    Basically the same thing I fixed in 12c611b12123.

commit 0090fcd26df521f3deb63bf9cf0ef9c54f2cf9ac
Author: Michael Norrish <[email protected]>
Date:   Mon May 6 12:06:38 2024 +1000

    Get developers/genUseScript to compile again (still wrong though)

commit c75093f7a9bdf34fb10002e1e50e0a0c1ec153fc
Author: Chun Tian (binghe) <[email protected]>
Date:   Sat May 4 00:00:57 2024 +1000

    FTBFS (NOT_ZERO is from "examples/algebra")

commit 865dbda999616b1f65a036055f0bfdbd1b0576e1
Author: Chun Tian <[email protected]>
Date:   Fri May 3 23:33:22 2024 +1000

    Update docker-ci.yml

commit 36d0b54855455d80bb7b61074495e31b75922a9c
Author: Chun Tian <[email protected]>
Date:   Fri May 3 23:32:56 2024 +1000

    Update docker-ci-for-pr.yml

commit 3fa1d37aa6ea8275d4dc7ac579bd750862c2b3c4
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri May 3 23:30:13 2024 +1000

    Fixed --otknl build (up to hol-base / boss) using old Arithconv.sml

commit 6c43d903d149104e34294be8ac0893a25ec24fd8
Author: Chun Tian (binghe) <[email protected]>
Date:   Sun Apr 28 12:56:10 2024 +1000

    Some wording fixes in TRANS_TAC.doc

commit e87d28cfab3b0aa611edef74c7785807ffe0c873
Author: Chun Tian (binghe) <[email protected]>
Date:   Sat Apr 27 12:26:15 2024 +1000

    TRANS_TAC ported from HOL-Light

commit 4b7d021796670f412b0423ef4465ef3453d92096
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri May 3 13:33:10 2024 +1000

    FTBFS (help)

commit e6ce07231667c75940e69090d0a4c5aea1700a8c
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri May 3 11:47:11 2024 +1000

    Move new files into subdirectories under src/algebra

commit 4387c34e4a1d0a578c04b759fe735a6dc08f2dda
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 30 18:49:16 2024 +1000

    Fixed building HOL manuals with PolyML (and not in --otknl)

commit 27e4453054f20589111f618f94dd065085b5e6b4
Author: Chun Tian (binghe) <[email protected]>
Date:   Thu Apr 25 21:09:27 2024 +1000

    FTBFS with Moscow ML

commit 675fcb139002ecf5f62b9f68e95872954da652b9
Author: Chun Tian <[email protected]>
Date:   Thu Apr 25 18:43:34 2024 +1000

    Update docker-ci.yml (add build-mosml)

commit 79a0a60484ceb97c9ad3a72b91bcb655aaa39c50
Author: Chun Tian <[email protected]>
Date:   Thu Apr 25 18:42:55 2024 +1000

    Update docker-ci-for-pr.yml (added build-mosml)

commit 82a9c2d8dfade24e2caa5513ba782d04dabc2f3c
Author: Chun Tian (binghe) <[email protected]>
Date:   Thu Apr 25 18:40:21 2024 +1000

    Updated Dockerfiles with necessary TeXlive packages for building HOL manuals

commit e006edd4c63dd1e725e8e19b18807bb13f96db1e
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 30 15:49:59 2024 +1000

    Fix bug in cv_typeLib (translation failed in limited grammar ctxts)

    Bug reported by “someplaceguy” on CakeML discord, giving the name for
    the regression test script.

    Library code was calling the global parser, which as we all know is a
    mortal sin.

commit 02a954437bfe96f7ba8b3f7f9271a680f441d927
Merge: a4084dad4 81398409d
Author: Chun Tian (binghe) <[email protected]>
Date:   Thu Apr 25 20:45:55 2024 +1000

    Merge remote-tracking branch 'origin/develop' into monoidTheory

commit 81398409d1dbb6e695c0df0a4e40be075fdd0477
Author: Michael Norrish <[email protected]>
Date:   Thu Apr 25 22:16:05 2024 +1200

    Produce new blank next-release.md file for what I assume will be T-2

commit fd366fde86123cf8d42ca2530fa10c15fbf14549
Merge: 6dbb43de3 2d798aea0
Author: Michael Norrish <[email protected]>
Date:   Thu Apr 25 22:13:47 2024 +1200

    Merge tag 'trindemossen-1' into develop

commit 2d798aea036cf23fe3f5b6ce5f939cb491a07119
Author: Magnus Myreen <[email protected]>
Date:   Tue Apr 23 10:16:35 2024 +0100

    Fix typo in the Description

commit 6dbb43de313fcb6db93fd69adce21ed024b76590
Author: Magnus Myreen <[email protected]>
Date:   Tue Apr 23 10:16:35 2024 +0100

    Fix typo in the Description

commit a4084dad40e8cc7e339ef97a149dcccd877b6ea1
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 23 11:21:43 2024 +1000

    FTBFS examples/lambda

commit 2da4265c965ef3ad80e39255b48657eb18e71210
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 23 10:31:06 2024 +1000

    Revert name changes of SNOC_LAST_FRONT for better backward compatibility

commit 112b2b69bb3f8b1b03f66f1a7ffe362b755ebc67
Author: Michael Norrish <[email protected]>
Date:   Mon Apr 22 16:48:19 2024 +1000

    Stamp current release notes as what's going into next release

commit 12c5f2ef701ef39c457840d4980b9af64392dcab
Author: Chun Tian (binghe) <[email protected]>
Date:   Mon Apr 22 05:07:05 2024 +1000

    Mention new algebra theories in next-release.md (using some words from examples/algebra/monoid/README.md)

commit 4630435c969379dc681d26c9243642fe1754641f
Author: Chun Tian (binghe) <[email protected]>
Date:   Mon Apr 22 04:19:06 2024 +1000

    Fixes of examples/lambda work due to one renamed theorem in rich_listTheory

commit d9c43039ffbc18492acec03e554caabc07f737c4
Author: Chun Tian (binghe) <[email protected]>
Date:   Mon Apr 22 03:45:18 2024 +1000

    Changes of examples/{AKS|fermat|simple_complexity} after src/algebra/monoidThoery

commit 6bd26f377211aafc174add159bb12258fe0646a7
Author: Chun Tian (binghe) <[email protected]>
Date:   Sun Apr 21 20:53:28 2024 +1000

    Algebra materials moved to core theories (up to monoid)

commit 12c611b12123da645e2d6dc86f640fe6cf52a981
Author: Michael Norrish <[email protected]>
Date:   Fri Apr 19 22:16:28 2024 +1000

    Fix Holmakefile INCLUDES error causing unnecessary HOL rebuilds

    You can't link back to src/ directories that precede boss because the
    system imagines that the source files there depend on hol.state and
    will promptly rebuild/recompile them, causing headaches later.

commit ef4c2c8c2f864b9de0079ff61299cdc6acc74964
Author: Anthony Fox <[email protected]>
Date:   Thu Apr 18 14:59:12 2024 +0100

    Rework IN_CONV implementation

    IN_CONV (used by EVAL) was suffering from performance issues related to excessive recursion (triggered through a "handle HOL_ERR _" that has been removed in the reworked version). In particular, IN_CONV was not working well for terms of the form:

    x1 INSERT x2 INSERT ... xn INSERT { y | P y }

commit 244c07da3e8592a9c4b1754a2c93c83f0da5759e
Author: Michael Norrish <[email protected]>
Date:   Thu Apr 18 17:17:44 2024 +1000

    Fix test broken by arrival of rationals into dependencies

commit 2dc54739f1fe5c0e2111b2b31c2d4a3953cc7f65
Author: Michael Norrish <[email protected]>
Date:   Wed Apr 17 13:44:46 2024 +1000

    Add INCLUDES line to bootstrap/Holmakefile to ensure parallel build

    As the dependency cv_transLib is also being built in parallel, the
    INCLUDES line is needed so that this directory is not attempted until
    cv_transLib is built.

commit 4fa4503bce3a147a36fbbfbd5ff7f96c61085c8d
Author: Michael Norrish <[email protected]>
Date:   Wed Apr 17 13:27:20 2024 +1000

    Adjust Holmake/theory-diagnostics to distinguish --fast from cheat

commit 81a7c2fd31c4a52cce0b34f0bf3841b54cf1edbe
Merge: 76ecb1d3d 7d8de5ca8
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 16 15:22:42 2024 +1000

    Merge pull request #1217 from HOL-Theorem-Prover/cv_translator

    cv translator

commit 7d8de5ca85588eb33fdfef5ccbae43337ef21704
Merge: 009088e4a 76ecb1d3d
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 16 15:21:14 2024 +1000

    Merge branch 'develop' into cv_translator

commit 76ecb1d3d4baae7343a97ebca2efc579346e08cc
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 9 20:26:11 2024 +1000

    More primitive definition of q_set (IMAGE real_of_rat UNIV)

commit 4291f88cd08bcff4dfb445b94219819cd9e8d00c
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 9 17:11:14 2024 +1000

    Attempt to fix dining_criptosTheory by deprecating int/rat

commit 25f45dd9f13bab5ede6f174cf1f1f46a52443961
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 9 15:35:01 2024 +1000

    Fix probability-related code after loading real_of_ratTheory by deprecating int and rat in term parser

commit 5adf5d00209d3b8bb7823571508df0f2a4eef395
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 9 15:33:00 2024 +1000

    Move q_set (real_rat_set_def) theorems from real_sigma to real_of_rat with duplicated proofs merged

commit e444dac45648885502641cd58deb351d0801121a
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Apr 9 15:03:20 2024 +1000

    [gcd,rat] theorems cherry-picked from the ongoing `cv_translator` branch (#1217)

commit 009088e4a9f26128af32d89a009bbaa54fd39480
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Apr 12 00:04:00 2024 +0100

    Try to fix regression

commit 4a79f07297aa0df05b94f1b10830f7dea7ee242d
Author: Hrutvik Kanabar <[email protected]>
Date:   Thu Apr 11 23:12:47 2024 +0100

    Fix a failing selftest

commit 6300798eaa05829e57d241ed36509d01cc4bcdae
Author: Hrutvik Kanabar <[email protected]>
Date:   Thu Apr 11 22:44:47 2024 +0100

    Uncheat cv translation in `examples/bootstrap`

commit 6d82d9940a51ba8f467b43b8347212f335c1489a
Author: Magnus Myreen <[email protected]>
Date:   Thu Apr 11 07:37:10 2024 +0200

    Fix a silly mistake in a cv_rep theorem

commit c297f94baeb53125e52a010f9b9659690241c944
Author: Magnus Myreen <[email protected]>
Date:   Thu Apr 11 05:04:58 2024 +0200

    Replace cv_sum_depth by cv_size (and delete cv_size_alt)

commit d2705cdc3fbddeaba656c955cab45b983c10dc28
Author: Magnus Myreen <[email protected]>
Date:   Thu Apr 11 04:45:53 2024 +0200

    Remove references to examples/bootstrap from examples/cv_compute

commit 1bc19e5b6cbb475ffca62ef85aa75fcc6a578372
Author: Magnus Myreen <[email protected]>
Date:   Thu Apr 11 04:14:40 2024 +0200

    Use cv_eval instead of EVAL

    Note that this commit leaves a cheat that needs removing.

commit 4c9b707ee09fa5cfedca6cfb6ebb91a371a8b447
Author: Michael Norrish <[email protected]>
Date:   Thu Apr 11 09:20:47 2024 +1000

    Fix proof failure caused by name generation change in 68ea515ce46a83

commit 3f0b36ca4c7c5d22459b0058ccb5452858d38a72
Author: Michael Norrish <[email protected]>
Date:   Wed Apr 10 22:00:55 2024 +1000

    Simplify transfer approach for monoids as types theory

    Vast majority of theorems transfer cleanly

commit 68ea515ce46a835a7086934dc099ebf02b5ec5fa
Author: Michael Norrish <[email protected]>
Date:   Wed Apr 10 21:56:11 2024 +1000

    Improve transferLib's choices for bound names (mimick source)

commit 4fbc78b13a185c10c1f054e79a41611c7318dcc0
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 9 18:24:34 2024 +1000

    Transfer more theorems semi-automatically to monoid as type theory

commit d27435acb96c050da315dd65676f0eaeb131a3c3
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 9 18:23:43 2024 +1000

    Sequence file to build core HOL up to point of parallelisation

commit 190392c28bd3f7aa723f97f973b8f575d999ecf0
Author: Chun Tian (binghe) <[email protected]>
Date:   Sat Mar 23 17:38:45 2024 +1100

    Fix uses of newtypeTools.rich_new_type in newly committed work

commit 4ec64bcc562d36bcceaec7e84097b7ddea18bc15
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri Mar 22 12:56:37 2024 +1100

    FTBFS rich_new_type{} in nomdatatype.ml

commit b9335aa4a16a20ada0af10816f16f345ad340e3d
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri Mar 22 12:34:59 2024 +1100

    More arguments (ABS, REP) of newtypeTools.rich_new_type

commit 84f2039b4b5161d752a757f7dbff0874ca65aebd
Author: someplaceguy <[email protected]>
Date:   Sat Mar 23 19:58:36 2024 +0000

    HolSmt: remove workaround for #1203

    Now that all known issues were fixed wrt. ARITH_PROVE not proving
    goals that COOPER_PROVE could, we can remove this workaround, thus
    making proof replay faster in some cases.

commit 70bec8c55cc072390806fc27ee3ff146c544b378
Author: someplaceguy <[email protected]>
Date:   Mon Mar 18 17:37:50 2024 +0000

    HolSmt: parse `assign-bounds` index in arith rules

    This commit fixes a parsing error when parsing arithmetic `th-lemma`
    inference rules with an `assign-bounds` parameter, i.e.:

    ((_ th-lemma arith assign-bounds ...) ...)

    The error was due to `assign-bounds` not being in the known term
    dictionary.

commit aee048a87d352226c758752e354bdcd769a18ce9
Author: someplaceguy <[email protected]>
Date:   Mon Mar 18 17:16:41 2024 +0000

    HolSmt: handle end-of-stream when parsing SMT-LIB files

    The SMT-LIB file parser was ending up raising an end-of-stream
    exception unless the `(exit)` command was present in the SMT-LIB file,
    even though the `(exit)` command does not seem to be mandatory
    according to the SMT-LIB v2.6 standard.

commit d4ab50df4c6ec588aa998aa5490710d18b39e7cb
Author: someplaceguy <[email protected]>
Date:   Mon Mar 18 15:28:46 2024 +0000

    HolSmt: parse `declare-const` commands

    Add support for parsing `declare-const` commands to the SMT-LIB
    parser.

commit 819ce3c3bafbf447bc46d97575447cd3fea088df
Author: someplaceguy <[email protected]>
Date:   Sun Mar 17 11:38:58 2024 +0000

    HolSmt: don't get rid of `quot` and `rem` in arithmetic rules

    It should not be necessary to rewrite these symbols with their
    definitions, because from the perspective of SMT solvers, these should
    just be functions like any others. Therefore, when replaying
    arithmetic proof steps, the proof handler should not need to
    understand what `quot` and `rem` are.

    This is a partial revert of the following commit:
    6220a17848fd58bcb54bb9df9df6b55d5859abf0

    It's not clear to me why I introduced this change in the first place,
    since the tests do work fine without it. Also, there doesn't seem to
    be any performance regression.

commit b8fa4ad3ffa7453a6f6cb2d49473224daff5b4c2
Author: someplaceguy <[email protected]>
Date:   Fri Mar 15 12:01:30 2024 +0000

    HolSmt: ignore indices in `rewrite` proof rules

    In case `rewrite` proof rules ever come to have indices, let's ignore
    them instead of erroring out.

commit 391faf850d46b9de4e09de6478e451ec87984a29
Author: someplaceguy <[email protected]>
Date:   Thu Mar 14 17:21:12 2024 +0000

    HolSmt: add `let`, `ediv` and `emod` simps to `thm_AUTO`

commit 055488c99a8a7c9dd7827c9e069dcaf87370f9e7
Author: someplaceguy <[email protected]>
Date:   Thu Mar 14 16:48:01 2024 +0000

    HolSmt: add full battery of `quot` and `rem` tests

commit 1a87909fc794783df8f1262ed73c5d8ff2fa2619
Author: someplaceguy <[email protected]>
Date:   Thu Mar 14 16:13:25 2024 +0000

    HolSmt: replay goals containing `quot` and `rem`

    HOL4's integer arithmetic decision procedures cannot handle `quot` and
    `rem`, so proof steps containing these symbols were failing to replay.

    This commit rewrites goals containing these symbols to increase the
    chances of a successful replay.

    `thm_AUTO` was similarly improved, as it had the same limitation and
    was failing to prove some of the self-tests.

commit 23af0d085f12415cfb179d54e647c3c878c1a916
Author: someplaceguy <[email protected]>
Date:   Thu Mar 14 12:28:42 2024 +0000

    HolSmt: remove workaround for NotFound exn in ARITH_TAC

    Now that #1209 is fixed, we can remove the workaround for it in
    HolSmt.

commit 72f09bbbae2e181e7fbab38c773e19ab87cbc8ea
Author: someplaceguy <[email protected]>
Date:   Thu Mar 14 12:25:37 2024 +0000

    HolSmt: use integerTheory's ediv and emod

    Now that integerTheory contains the definitions for Euclidean div and
    mod, let's use that instead of redefining these operators in
    HolSmtTheory.

commit b5d90204b1ce9320ca8724010b116b3961fed5b1
Author: someplaceguy <[email protected]>
Date:   Thu Mar 14 12:01:51 2024 +0000

    Add Euclidean div and mod, plus some num/int theorems

commit eddeef51c3ad8343b9642a3fcbe8191ea23d97bd
Author: someplaceguy <[email protected]>
Date:   Thu Mar 14 02:22:04 2024 +0000

    HolSmt: fix workaround for extra hypothesis in proof replay

    The previously-implemented workaround might have an issue where if Z3
    introduces an hypothesis of the form `P = P` but then *doesn't* forget
    to discharge it, we might fail to replay the `lemma` proof rule
    because we avoided adding an assumption.

    Instead, this commit fixes the workaround so that we remove the extra
    hypothesis at the end of the proof replay procedure, i.e. only when we
    are sure that Z3 *did* forget to discharge the hypothesis.

commit a30d4a4276ab4e511759b5aa37aaf4c668695649
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 14:55:08 2024 +0000

    HolSmt: update documentation

commit 4b596255753e0c57fab7f386fd567a2f9e45c47c
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 12:10:32 2024 +0000

    HolSmt: try harder to replay arithmetic proof steps

    This commit adds some tactics which help prove some arithmetic proof
    steps that intLib.{ARITH,COOPER}_TAC can't deal with.

    These are basically some workarounds for:

    https://github.com/HOL-Theorem-Prover/HOL/issues/1207

    This allows us to enable proof replay for the remaining arithmetic
    test cases that didn't already have proof replay enabled, with the
    exception of the very last test case (because we can't replay
    nonlinear arithmetic proof steps).

    That said, I don't expect these workarounds to be very reliable.

    Ideally, it would be better to improve HOL4's linear arithmetic
    decision procedures.

commit 1a0145aa2b01864cf7dacae4af64f50ff9ae1bc2
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 10:39:08 2024 +0000

    HolSmt: merge z3_lemma_arith and z3_rewrite's arith

    Since these two decision procedures need to handle the same kind of
    terms (including smtdiv / smtmod rewrites), this commit merges them.

commit d3c92d76638ab87aa0abd0666222c22b0bde2d0b
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 09:43:12 2024 +0000

    HolSmt: work around Z3 bug in `hypothesis` proof rule

    In some proof certificates, Z3 emits a `hypothesis` inference rule
    without discharging it later with a `lemma` rule. This causes some
    proofs to fail at the end of the proof replay procedure, because
    they end up containing an extra hypothesis.

    Fortunately, so far all such undischarged hypothesis rules were of the
    form `p = p`, so for now we can easily work around this issue by
    creating such theorems without adding an assumption.

    This workaround allows us to enable proof replay for 5 more
    self-tests.

commit ec98ab611a41c3643d00986ccc55ced58d9049ef
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 09:25:57 2024 +0000

    HolSmt: work around NotFound exn in ARITH_PROVE

    This commit contains a workaround for the following issue:

    https://github.com/HOL-Theorem-Prover/HOL/issues/1209

commit e903f05e498126f29731c7ee5203da5f0f268de9
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 09:13:39 2024 +0000

    HolSmt: enable the remaining div and mod tests

commit 19c2c262c61864d0b7d6063c67891e2a38ab19c8
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 06:53:15 2024 +0000

    HolSmt: implement `iff-false` Z3 proof rule

commit c4c184a688f131ecc3f3216887f2d9cbb94838f5
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 05:57:33 2024 +0000

    HolSmt: major fixes for Z3 replay of `th_lemma_arith` rule

    The `th_lemma_arith` was running into several issues. The following
    changes were made:

    1. The `generalize_ite` procedure was removed, since the arithmetic
    decision procedures can handle `if ... then ... else ...` now. It was
    causing replay failures because some terms were not provable unless
    the decision procedures could inspect the `if` bodies.

    2. The arithmetic decision procedures don't understand `smtdiv` and
    `smtmod`; so before proving the term, we now rewrite it with the
    definitions of these functions.

    3. A workaround was also implemented for some instances of the
    following issue:

    https://github.com/HOL-Theorem-Prover/HOL/issues/1207

    Namely, the integer decision procedures cannot decide some terms
    containing `ABS` and `Num`, so we rewrite them when possible.

commit 8d6e54bd5aa0bab7ab96a77a066672babfdd80c8
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 03:58:22 2024 +0000

    HolSmt: parse `div0` and `mod0` in Z3 proofs

    Unfortunately, these operators don't seem to be documented.

    However, from a quick reading of the Z3 source code, it seems that
    they seem to be similar to `div` and `mod`, but they seem to be used
    to indicate that Z3 can't prove that the divisor is non-zero.

commit a2f47a923362ee9cf921731134034340380e3b82
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 03:38:41 2024 +0000

    HolSmt: enable DIV tests

commit 4ca0db5b762ee280b8ee0376e6923aec666e81cd
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 03:16:29 2024 +0000

    HolSmt: add some arithmetic theorems

    SMT_NUM_ADD and SMT_NUM_SUB were meant to be used in place of INT_ADD
    and INT_NUM_SUB for optimization reasons.

    However, this causes a regression in proof replay in one of the
    self-tests. Since this regression is not straightforward to fix,
    these theorems are not being used yet.

    NUM_OF_INT was also added to the default set of theorems since it
    helps solve some `num`-related goals.

commit 48b39a8f98f4f0c5a6aaffc7dd340835935e7034
Author: someplaceguy <[email protected]>
Date:   Tue Mar 12 03:04:16 2024 +0000

    HolSmt: fix hang in arith Z3 proof replay

    The previous workaround for ARITH_PROVE failing to prove some terms
    changed the `th_lemma_arith` proof handler to use COOPER_PROVE
    instead.

    However, COOPER_PROVE sometimes is too slow and appears to hang when
    replaying some Z3 proofs.

    This commit changes the `th_lemma_arith` handler to first try
    ARITH_PROVE which is much faster, and only if it fails, then try
    COOPER_PROVE.

commit dba3657acffebd68ad8fb34d0ab8569e0fb9c9e8
Author: someplaceguy <[email protected]>
Date:   Sun Mar 10 01:07:10 2024 +0000

    HolSmt: add support for div and mod

commit 7ef04d38a121fd9082a8652ae6150ce1abc95366
Author: someplaceguy <[email protected]>
Date:   Mon Mar 11 02:40:48 2024 +0000

    HolSmt: fix `let ... and ...` SMT-LIB translation

    The SMT-LIB term translator couldn't handle parallel definitions
    properly. This commit fixes that.

commit 8605071187e3c0ef971cddef84a24a5675764bfa
Author: Chun Tian (binghe) <[email protected]>
Date:   Wed Mar 27 14:28:02 2024 +1100

    [combin] Add one more theorem: EXTENSIONAL_RESTRICTION

commit cf6d9862da6d2e4f113bfe7148118503c570658c
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri Mar 22 15:08:21 2024 +1100

    EXTENSIONAL and RESTRICTION ported from HOL-Light

commit 65f2a59f55f5c55ae2c6ce188a1269e1618bd94b
Author: Magnus Myreen <[email protected]>
Date:   Sat Apr 6 05:27:22 2024 +0200

    Generate small numbers only once in thm/Compute.sml

commit 7ec599db91151b3c6a6bad0b092bdc1c2c7d50ea
Author: Magnus Myreen <[email protected]>
Date:   Sat Apr 6 05:20:15 2024 +0200

    Make Thm.compute do more earlier

commit 22300a65f94b48536e01a7e9be50b927e85d0d19
Author: Magnus Myreen <[email protected]>
Date:   Sat Apr 6 03:41:58 2024 +0200

    Make Thm.compute accumulate thm tags

commit 738ed9400c7d3bc2ca6b7cda70f65773c83b4c93
Author: Michael Norrish <[email protected]>
Date:   Wed Apr 3 20:36:49 2024 +1100

    Fix bug in SWAP_EXISTS_CONV (manifested in Cooper's d.p. in integer)

commit a925fed59eccd6d257c42d2a5d88d2ce7429f6ed
Author: Magnus Myreen <[email protected]>
Date:   Thu Apr 4 04:23:03 2024 +0200

    Make sure "cv_" appears before theory name prefix

commit 2875e0cbdd7bba461a4d893a0a38f34c73a63b2c
Author: Magnus Myreen <[email protected]>
Date:   Thu Apr 4 04:08:47 2024 +0200

    Use cv_trans instead of cv_trans_pre in a few places

commit 4d623c3e0ede1afab926cae9fe4680475b8d6584
Author: Magnus Myreen <[email protected]>
Date:   Thu Apr 4 04:08:00 2024 +0200

    Avoid name clashes in cv_transLib

commit 3fa79893fb30ba3225975b8ef528ca4d2c6ecf55
Author: Michael Norrish <[email protected]>
Date:   Wed Apr 3 14:06:41 2024 +1100

    Fix INCLUDES line in src/finite_maps/Holmakefile

    Knock-on from a4d582152a. Thanks to Chun Tian for report of problem.

commit 798d323a82e0c012aa981b4d9978d6642fef9034
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 2 14:22:55 2024 +1100

    Test-case tweaks given 9edfb8164e5c04ac

    ASCII arrows get replaced by \HOLTokenMap{} and some linebreaking
    changes as a result also.

commit a4d582152a96076cd18c887a983f5be0224c7806
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 2 11:39:33 2024 +1100

    Handle |-> token for TeX p/printing in finite_maps better

    Now the same TeX notation is used for the |-> in “:'a |-> 'b” and in
    “f(| k |-> v |)”.

commit 9edfb8164e5c04aca3d09b71f3c736c1225ddc20
Author: Michael Norrish <[email protected]>
Date:   Tue Apr 2 11:38:51 2024 +1100

    Get TeX p/printing to do nice LaTeX for types (arrows and Greek)

commit 13c94a2f00a7c40cae8579e5b4eb9f451ade661f
Author: Magnus Myreen <[email protected]>
Date:   Sun Mar 31 07:35:16 2024 +0200

    Avoid [] pretty printing as epsilon

commit b53822e18dcfb4bf9d4267afa9a310614bf5b940
Author: Hrutvik Kanabar <[email protected]>
Date:   Tue Mar 26 14:12:37 2024 +0000

    Some fixes

    - Unicode violations
    - Missing `INCLUDES` in `Holmakefile`
    - Update a `README`

commit b7051d3b53f58d5f4db06272afbafdbfa9bebdc8
Author: Michael Norrish <[email protected]>
Date:   Tue Mar 26 18:07:31 2024 +1100

    Provide TeX notations for function update syntax

commit f57070d427868aa51f38b29eabf4353ceabb7a5e
Author: Hrutvik Kanabar <[email protected]>
Date:   Sat Mar 23 14:20:23 2024 +0000

    Sketch `cv_transLib` entry in Description

commit ddf702878b2cc0ea0830738ee0631b0e72da57e9
Author: Hrutvik Kanabar <[email protected]>
Date:   Sat Mar 23 14:20:23 2024 +0000

    Pass through docfiles

commit 9e8cb30bf8756b6c7bae0ca2ba897b7344026c18
Author: Michael Norrish <[email protected]>
Date:   Sat Mar 23 10:36:42 2024 +1100

    Start of some work on "algebras as types"

    Starting with the base of the algebra pyramid keeps things simpler,
    and will hopefully allow the technology to be worked out and polished.

commit 55c6eca980922f551a135a65496c07ec603fd52e
Author: Michael Norrish <[email protected]>
Date:   Fri Mar 22 20:12:04 2024 +1100

    Implement a xfer_fwd_tac for transferLib

commit ce133ee32087143dbe61b7c81c4948f10d82c7da
Author: Michael Norrish <[email protected]>
Date:   Fri Mar 22 20:11:09 2024 +1100

    Define extend fn to extend a monoid's carrier to all of type

commit 44bb8cea085b9993b36885f7a2f69610063c6b86
Author: Michael Norrish <[email protected]>
Date:   Fri Mar 22 20:10:04 2024 +1100

    Mention polarity search in release notes

    This was implemented in PR #1208

commit 591cfcf1656d67f4d28fce86854c800f22f93956
Author: Michael Norrish <[email protected]>
Date:   Fri Mar 22 20:07:23 2024 +1100

    Fix another bug in Omega d.p.

    Thanks to someplaceguy for reporting these.

    Progress of sorts with github issue #1207

commit e546764f153c268543103c60ed61bd9941768e05
Author: Chun Tian (binghe) <[email protected]>
Date:   Wed Mar 20 14:57:39 2024 +1100

    Speedup examples/probability building process

commit f97f4ffa7db4a7929723438df248a180bd1b435b
Author: Chun Tian (binghe) <[email protected]>
Date:   Tue Mar 19 11:50:05 2024 +1100

    Fixed TeX munge outputs of NegInf (extreal)

commit 6252f430c58963c182efc0f3e6cc690dc3631a4a
Author: Chun Tian (binghe) <[email protected]>
Date:   Mon Mar 18 23:22:55 2024 +1100

    Added algebra_finite_subsets_imp_sigma_algebra, etc.

commit 3c8a6cb48a5cb437988afe41dc0933480fcc5ee4
Author: Chun Tian (binghe) <[email protected]>
Date:   Mon Mar 18 11:59:01 2024 +1100

    Minor fix & updates to probability materials

commit dd274cc494f343180dc4e8406d93ee7b96e46f63
Author: Chun Tian (binghe) <[email protected]>
Date:   Thu Mar 14 19:05:56 2024 +1100

    [lambda] Boehm_out_lemma (Proposition 10.3.7 (i) [1, p.248])

commit 5a607569d2a0fd0abe15add18996f1709aff1241
Author: Eric Hall <[email protected]>
Date:   Tue Mar 19 22:58:46 2024 +1100

    Allowing user to choose between positive polarity matching and negative polarity matching by providing a prefix argument

commit 1321abd20bd7245fec98bb448f98ed33795bc861
Author: Eric Hall <[email protected]>
Date:   Tue Mar 19 18:26:30 2024 +1100

    Fixing issue where unicode symbol was being used where this was not permitted

commit 7ac3d89624a1d893b31a32fdefe1180b06916031
Author: Eric Hall <[email protected]>
Date:   Mon Mar 11 22:27:18 2024 +1100

    Fixing silly bug which prevented polarity search from working

commit a8f13229afe5e39ca05f37815bbb6d3ae4a6c35c
Author: Eric Hall <[email protected]>
Date:   Sat Mar 9 22:33:50 2024 +1100

    adding code to use hotkey to search for theorems based on terms in premises and conclusions

commit d6cc90288bffbd6a1807302e291235ac866a2efb
Author: Eric Hall <[email protected]>
Date:   Sat Mar 9 20:49:06 2024 +1100

    Writing code to allow theorems to be searched based on what terms appear as premises or conclusions to those theorems, rather than simply testing whether a particular term is present in the theorem anywhere.

commit 1a1b46d9be426307029882cb1e3bcfbdaf0c43a1
Author: Michael Norrish <[email protected]>
Date:   Tue Mar 19 17:28:48 2024 +1100

    Handle natural number subtraction under & better in int d.p.'s

    Addresses a couple of cases from github issue #1207

commit 5788053992c2aff5952489f5367121dac8cdbff2
Author: Michael Norrish <[email protected]>
Date:   Tue Mar 19 15:55:05 2024 +1100

    Fix handling of Num in line with its new semantics

    Possible because of 55230652bbe9

    Closes #1203

commit 671b4b712f9e860a558393b4b0c6a15e3a52a754
Author: Chun Tian (binghe) <[email protected]>
Date:   Wed Mar 13 22:41:51 2024 +1100

    Updated HOL Description with higher mathematics contents promoted to chapter level

commit 9ac238fdf4bfbd20dd4c90d977c3f4a137c36287
Author: Matthew Richards <[email protected]>
Date:   Wed Mar 13 14:19:18 2024 +1100

    Add clearer error on double implication in inductive definitions

    Previously a more cryptic error would be raised here; now it should
    be diagnosed that conjunctions are to be used instead.

commit 424be5497b74891ab006a67b5c809a3943d23305
Author: Hrutvik Kanabar <[email protected]>
Date:   Sun Mar 17 17:54:04 2024 +0000

    Add a random sptree lemma

commit 23a41fbb4d1034fcddba3dd82ce9c4fbde586b7e
Author: Magnus Myreen <[email protected]>
Date:   Sun Mar 17 22:38:36 2024 +0100

    Make cv_*trans_rec return unit

commit e63c18572a7d5796e1f419c6d870d0e5a5391416
Author: Magnus Myreen <[email protected]>
Date:   Sun Mar 17 21:36:28 2024 +0100

    Write some doc files for cv_trans functions

commit e8de5684760f5fb51d4cae7992feb21bdf016e40
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Mar 15 16:55:23 2024 +0000

    Add a cv docfile

    Co-authored-by: Magnus Myreen <[email protected]>

commit 5188e60f751cd0e86ec4a231d93cba6ad07391f9
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Mar 15 10:53:10 2024 +0000

    Expand on cv text in `next-release.md`

    Co-authored-by: Magnus Myreen <[email protected]>

commit 0b944581367edae0f87be5e61e2684d2117f6ed4
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Mar 15 16:00:42 2024 +0000

    Copy over cv translator examples from CakeML/cakeml#985

commit 542fc78f63b80f52c5b0ce357999104b98a5344f
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Mar 15 15:55:55 2024 +0000

    Delete old cv examples

commit fc160dde5f557fa0a0c7def21fd5722bee09c08e
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Mar 15 15:53:00 2024 +0000

    Move some theorems to appropriate theories

commit 02e4b212fe47e70e04b32f4d982d239b9ca1b5ce
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Mar 15 10:53:10 2024 +0000

    Move a few cv functions

    Co-authored-by: Magnus Myreen <[email protected]>

commit a7babafe2cfc2ac6ec2e583e5cd8ad411a13a62f
Author: Hrutvik Kanabar <[email protected]>
Date:   Fri Mar 15 10:53:10 2024 +0000

    Copy over cv translator work from CakeML/cakeml#985

    Co-authored-by: Magnus Myreen <[email protected]>

commit 9f96ab9d68b28bc65d470932346d72c4a17ac605
Author: Michael Norrish <[email protected]>
Date:   Fri Mar 15 16:39:35 2024 +1100

    Document DB.selectDB; tweak doc file for DB.find

commit cf3fab22e341c82a4dc94399c23c0fc062b65816
Author: Michael Norrish <[email protected]>
Date:   Fri Mar 15 15:47:38 2024 +1100

    Clean up some doc-files; preferring not to use alpha --> bool syntax

    This is a little confusing for new users who may not appreciate that
    types are typically obtained by calling the parser (“:...” syntax).

commit 01d5d9a7f4d32b0d18003f956a45f226dd43badd
Author: Michael Norrish <[email protected]>
Date:   Fri Mar 15 15:45:12 2024 +1100

    Fix bug in holfoot that let its parser get contaminated by others'

    In particular, its parsing referred to term_grammar() which let
    changes in other theories (in this case HolSmt) contaminate its
    namespace. Fix is to make sure its parsing is done with
    holfootTheory.holfoot_grammars (its own relatively fixed grammars).

commit e8b31786a24bec9b97777b614e69d558846a3b60
Author: Michael Norrish <[email protected]>
Date:   Thu Mar 14 17:32:11 2024 +1100

    Fix bug in Omega test

    Make slight changes to code along the way; making it easier to see
    state of dictionary that is used internally.  Bug was in call to
    one_var_analysis where a stale map variable (ptree) was used, when the
    correct parameter was (pt) which was the continuation's parameter.

    Add a number of test-cases, all of which are probably more or less
    equivalent.

    Thanks to someplaceguy for the bug report!

    Closes #1209

commit b9bd54bebaa9faa2874dc92ee667d148f2770384
Author: Michael Norrish <[email protected]>
Date:   Wed Mar 13 16:15:15 2024 +1100

    Upgrade integer DP testing code to use testutils

commit eeb10e889818e1f3fbaafad49ecb125de7280bda
Author: Michael Norrish <[email protected]>
Date:   Wed Mar 13 16:13:03 2024 +1100

    Fix a bug in PIntMap.size

commit 29e263e51c911f218102d767840a34bc7cb1b2df
Author: Chun Tian (binghe) <[email protected]>
Date:   Sat Mar 9 13:51:02 2024 +1100

    Better statements of Boehm_transform_exists_lemma

commit 5314eb3da47a6c5426a1337fdf960a150fc1f650
Author: Chun Tian (binghe) <[email protected]>
Date:   Fri Mar 8 15:43:32 2024 +1100

    [lambda] Boehm_transform_exists_lemma (Lemma 10.3.6 (ii) [1, p.247])

commit fbaa3a988821dfedb37377814ae537fd6855e3ab
Author: someplaceguy <[email protected]>
Date:   Sat Mar 9 19:27:13 2024 +0000

    HolSmt: fix Z3 proof replay of `asserted` proof rules

    This commit contains both a fix and a workaround for replaying
    `asserted` proof rules.

    The fix consists in disabling the `pp.simplify_implies` Z3 parameter.
    This parameter controls whether the Z3 AST pretty-printer does some
    simplifications when printing the proof and is enabled in Z3 by
    default.

    However, these simplifications can effectively mangle the terms in the
    `(asserted ...)` inference rules, which means they will not match the
    terms that were actually asserted in the input file (i.e. the terms in
    the assumptions of the goal). Therefore, these mangled terms would
    cause proof replay to fail in some cases.

    Unfortunately, in currently released versions of Z3 (i.e. 4.12.6 and
    earlier) it is not actually possible to disable `pp.simplify_implies`
    when printing the proof. A fix for this issue was submitted as the
    following PR:

    https://github.com/Z3Prover/z3/pull/7157

    To mitigate this parameter not currently working in Z3, a workaround
    was also implemented which tries to remove mangled asserted
    statements, which would end up as extra hypotheses in the final
    theorem.

    This workaround has been confirmed to work in Z3 v4.12.6 as well as Z3
    v2.19.

    Since this issue has been fixed, we can now enable two more self-tests.

commit c725a1a758751f12ac9feaeaa7cd80fc9cd5c8c9
Author: someplaceguy <[email protected]>
Date:   Sat Mar 9 04:41:09 2024 +0000

    HolSmt: add four rewrite theorems for Z3 proof replay

    This allows us to enable proof replay for one more self-test.

    Another self-test was added that exercises at least two of these
    theorems that the other self-tests don't.

commit 823e6496a30dd2c10dd5456295223e575887563b
Author: someplaceguy <[email protected]>
Date:   Sat Mar 9 04:22:55 2024 +0000

    HolSmt: replay `sk` inference rule in Z3 proofs

    This proof handler implements the following inference rules:

    |- ~(!x. P x y) <=> ~(P (sk y) y)
    |- (?x. P x y) <=> P (sk y) y

    The implementation is complicated due to the need to create the
    Skolem terms and due to the need for higher-order matching.

    Z3 proof replay was enabled for one more self-test.

commit f3f5e21f6213772ce745ccf70c06d442f34b04a5
Author: someplaceguy <[email protected]>
Date:   Fri Mar 8 23:19:51 2024 +0000

    HolSmt: fix `elim-unused` proof rule to work w/ `exists` quantifiers

    The `elim-unused` rule handler could only handle `forall` quantifiers.
    However, Z3 also uses it for `exists` quantifiers.

    This commit makes the handler work with both quantifiers, including
    when they are interspersed with each other.

    This fix is necessary for replaying an `elim-unused` rule in the Z3
    proof for the following self-test:

    ?x. x = x

    This commit also enables proof replay for the above self-test, since
    the proof can now be fully reconstructed.

commit c488a6c95a397379f61bf76b997fb31356d5b83e
Author: someplaceguy <[email protected]>
Date:   Fri Mar 8 22:38:06 2024 +0000

    HolSmt: fix `quant-intro` proof rule to work w/ `exists` quantifiers

    The `quant-intro` rule handler could only handle `forall` quantifiers.
    However, Z3 also uses it for `exists` quantifiers.

    This commit makes the handler work with both quantifiers, including
    when they are interspersed with each other.

    This fix is necessary for replaying a `quant-intro` rule in the Z3
    proof for the following self-test:

    ?x. x = x

commit 466d6c224a2db972ce86d30971e8fcbd788162a6
Author: someplaceguy <[email protected]>
Date:   Thu Mar 7 21:46:30 2024 +0000

    HolSmt: build an smtheap

    This reduces the loading time of HolSmtLib from around 42s to
    about 5s (on my laptop).

commit 68f30d60a1586c1fb27f53effa6e12adc98023b9
Author: someplaceguy <[email protected]>
Date:   Wed Mar 6 02:12:10 2024 +0000

    HolSmt: enable Z3 proof replay of `num` self-tests

    Due to all the recent fixes and improvements in the Z3 proof
    certificate parser and replay code, we can now replay these proofs
    correctly, so we can enable these tests (for Z3 v4 only, as these Z3
    v2 proof certificates contain undeclared terms that we are not able to
    replay).

commit 9f055e47f9a0dca4f65fa8e073275f3c16ba9c23
Author: someplaceguy <[email protected]>
Date:   Thu Mar 7 14:57:47 2024 +0000

    HolSmt: work around Z3 quant-inst proof rule issue

    This is a quick workaround for the following Z3 issue:

    https://github.com/Z3Prover/z3/issues/7154

commit 194563d5a050d34234035a7246502661adc7bb06
Author: someplaceguy <[email protected]>
Date:   Wed Mar 6 17:13:44 2024 +0000

    HolSmt: work around ARITH_PROVE bug

    This is a workaround for the following issue:

    https://github.com/HOL-Theorem-Prover/HOL/issues/1203

    When the above issue is fixed, this commit can be reverted.

commit 7724583437d63ccc97dca5d13b4719e5e4cc35cd
Author: someplaceguy <[email protected]>
Date:   Wed Mar 6 01:16:58 2024 +0000

    HolSmt: parse `proof-bind` rules in Z3 proofs

    These appear not to have any semantic value despite the Z3 v4.12.4
    source code implying that it either introduces lambda abstractions or
    `forall` quantifiers, depending on the interpretation.

commit 355248c6a3d8dfb4f5021c84a43934b6f477dae2
Author: someplaceguy <[email protected]>
Date:   Wed Mar 6 00:54:26 2024 +0000

    HolSmt: replay `refl` inference rule in Z3 proofs

    Also, parse the `~` operator when used as `equivalence modulo naming`.

commit 1c6e508280b9602107f0cd0ffde897bcd4f1526b
Author: someplaceguy <[email protected]>
Date:   Tue Mar 5 21:40:20 2024 +0000

    HolSmt: parse `lambda` binders in Z3 proofs

    These seem to be a local declaration of variable names+types that
    apparently are meant to be interpreted as free variables in the
    enclosed term.

    Note that these `lambda` binders should only be parsed when parsing
    Z3 proof certificates, as the SMT-LIB language as specified in the
    current 2.6 version of the standard doesn't actually have these
    binders and we don't want to parse identifiers coincidentally named
    `lambda` as these special binders in this case.

    We take advantage of the previously-implemented parser parametrization
    to determine whether `lambda` binders should be parsed or not.

commit 193cfe1c332b2859b4fbb354d4141b27af61fb6c
Author: someplaceguy <[email protected]>
Date:   Tue Mar 5 19:57:12 2024 +0000

    HolSmt: parse nested `let` bindings in Z3 proofs

    Z3 proof certificates contain `let` definitions nested within other
    `let` definitions.

    The SMT-LIB parser would parse these as HOL4 `let` terms, but we don't
    actually want to create those. Instead, we just need to bind the
    definitions to the names.

    Since the SMT-LIB parser can now be parametrized by `let` handling
    functions, we make use of this new functionality to parse `let` terms
    differently when parsing Z3 proof certificates.

commit 16e6d9426c44fb142c0715da0c0c54551966b69c
Author: someplaceguy <[email protected]>
Date:   Tue Mar 5 19:21:30 2024 +0000

    HolSmt: parametrize the SMT-LIB parser by `let` handling functions

    The SMT-LIB term parser and Z3 proof certificate parser are similar
    in most ways, but they need to handle `let` terms differently.

    To avoid having to duplicate a significant portion of the parser,
    this commit parametrizes the SMT-LIB parser so that it can handle
    these `let` expressions differently based on parser handling
    functions that are passed by the caller of the term parser.

    In this commit, only the SMT-LIB version of the `let` handling
    functions are implemented, so it doesn't change how the parsers work
    yet.

    However, in a subsequent commit, the Z3 proof parser will use this new
    functionality to parse the proof certificates correctly.

commit 0fb203fde51288bd3536e1e430d4c38098cf3441
Author: someplaceguy <[email protected]>
Date:   Wed Mar 6 00:35:53 2024 +0000

    HolSmt: rename nums -> indices

    Since indices are not necessarily numerals now, it's probably better
    to rename these function arguments.

commit 9640aeee1360656094181e76ccc68c4047de0642
Author: someplaceguy <[email protected]>
Date:   Sun Mar 3 17:30:30 2024 +0000

    HolSmt: replay `quant-inst` rule in Z3 v4 proofs

    It is an inference rule that creates the following proof:

    ------------------------------------------  QUANT_INST [u1,...,un]
      |- ~(!x1...xn. t) \/ t[u1/x1]...[un/xn]

commit f51b78741843c13b151b2b2cac1f06c5890af64a
Author: someplaceguy <[email protected]>
Date:   Sat Mar 2 18:06:20 2024 +0000

    HolSmt: parse indexed identifiers' indices as terms

    Prior to SMT-LIB 2.5, the indices of indexed identifiers could only
    be numerals.

    In SMT-LIB 2.5 and later, identifiers can be indexed not just with
    numerals but also with symbols. This was implemented in commit
    8a2e9bc97c2955bdbda0bceb90948e87a92f5c22

    However, the `quant-inst` inference rule in Z3 v4 proofs can contain
    arbitrary terms as its indices, as seen in this example:

    ((_ quant-inst (v12 v17) (v11 v17 ?x304)) ...)

    In order to add support for this rule in a follow-up commit, the
    SMT-LIB parser was changed to support arbitrary terms as indices in
    term identifiers (but not type identifiers).

    This should be a superset of what SMT-LIB allows, which should be fine
    because we don't need to implement a strict parser.

    However, Z3 v2 proof certificates contain inference rules such as the
    following:

    (_ |th-lemma| arith farkas -41/42 -1)

    In particular, `-41/42` and `-1` are not valid SMT-LIB terms. We used
    to parse this successfully because we allowed arbitrary strings as
    indices, but since we are trying to parse terms, this is now being
    rejected by the parser.

    Due to this regression, proof replay for some test cases was disabled
    for Z3 v2 (but they are still enabled for Z3 v4).

commit 043537b739e1b3a8de19e345630b587e1660d1d0
Author: someplaceguy <[email protected]>
Date:   Sat Mar 2 01:54:38 2024 +0000

    HolSmt: replay `mp~` proof rule in Z3 v4 proofs

    It's the same as the `Thm.EQ_MP` inference rule in HOL4.

commit 8932bbb3a745a23bb867f80badfa011d2dd04a9f
Author: someplaceguy <[email protected]>
Date:   Sat Mar 2 01:48:39 2024 +0000

    HolSmt: print invalid proofterms

    It's quite useful when debugging the usage of a proofterm that is
    missing in the proofterm dictionary.

commit c49e07bd42564a2cf9e267cb819d8a30eecc7b95
Author: someplaceguy <[email protected]>
Date:   Sat Mar 2 01:12:11 2024 +0000

    HolSmt: replay the `nnf-neg` and `nnf-pos` proof rules

    These should create proofs of negative normal form (NNF) steps.

    For the initial implementation, we rely on `metisLib.METIS_TAC` to
    find these proofs. If it becomes a bottleneck, a more specialized
    implementation could be developed.

commit 7aea54b0522c7fa3a6ab8a78ab57b706514e498f
Author: someplaceguy <[email protected]>
Date:   Thu Feb 29 21:46:40 2024 +0000

    HolSmt: make sure `let` definitions use unique names in Z3 proofs

    This commit adds code to check that Z3 proof certificates use unique
    names in `let` definitions.

    This is especially important to check now that some `let` definitions
    in Z3 proofs don't have its scope open until the end of the proof.

commit cc836c940b3592b1044cf2f9e4d45edefe75fc8a
Author: someplaceguy <[email protected]>
Date:   Thu Feb 29 01:04:12 2024 +0000

    HolSmt: hoist Z3 proof `let` parsing into separate function

    This is the initial step in making the proof certificate parsing more
    flexible. It doesn't change how the proof certificates are parsed, but
    this small refactoring will make it easier to make some improvements
    that are planned for later.

commit 72c0ab0a6835be5f76e503275f8b8169204571b5
Author: someplaceguy <[email protected]>
Date:   Wed Feb 28 23:41:00 2024 +0000

    HolSmt: disable Z3 v2 on failing test cases

    Z3 v2 is now failing in some tests due to fallout of some previous
    changes that were needed to add support for the `num` type.

    There are 2 root causes for these failures:

    1. Z3 v2 doesn't know about the integer `ABS` function. We used to
    rewrite the conclusion of the goal with the `INT_ABS` theorem but this
    is not needed when using modern SMT solvers because SMT-LIB supports
    `ABS` natively.

    2. Due to changes in how some goals are passed onto the SMT solvers,
    Z3 v2 is now generating proof certificates with some undeclared and
    untyped terms which we are not able to reconstruct.

    While I don't yet see a compelling reason to actively remove support
    for Z3 v2 (since support for Z3 v4 is mostly a superset of our support
    for Z3 v2), I don't see a compelling reason for adding v2-specific
    workarounds either, due to how old it is and due to it being
    unsupported for many years already.

    This commit adds new `thm_Z3_v4` and `thm_Z3p_v4` functions which only
    run the test cases if Z3 is configured and is version 4. These new
    functions are used in the test cases which succeed with Z3 v4 but not
    with Z3 v2.

commit 62097611c00799ddef1f5c78fa710a90fb4af811
Author: someplaceguy <[email protected]>
Date:   Sun Feb 25 22:07:24 2024 +0000

    HolSmt: add support for the `num` type

    This commit adds support for SMT solvers to reason about the `num`
    type by providing them with some theorems which allow them to convert
    `num` operations into integer operations which they natively support.
    Specifically, it adds to the proving context (as assumptions) theorems
    for the following conversions between `num` terms and integers:

    * `num` literals [INT_OF_NUM]
    * `SUC`, i.e. ``&SUC n <=> &n + 1i`` [INT]
    * `num` equality [INT_INJ]
    * `num` inequalities [INT_LE, INT_LT, GREATER_DEF, GREATER_EQ]
    * Non-negativity of `num` terms [INT_POS]
    * `num` addition and multiplication [INT_ADD, INT_MUL]
    * MIN and MAX [INT_MIN, INT_MAX]

    This is not an exhaustive list of all the theorems that will be
    needed to reason about the `num` type or even just `num` arithmetic,
    but it does allow Z3 to solve all the `num`-related self-tests, with
    the notable exception of DIV and MOD operators. To fix the latter, we
    will need to add support for integer division and mod first.

    Unfortunately cvc5 cannot solve a few of the `num` tests and the Z3
    proof reconstruction fails for almost all `num` tests, although this
    is not due to unsoundness in `num` support, but rather because the Z3
    proof certificates for these goals are more complex and use new proof
    syntax and rules which we do not support yet (this will be fixed
    later).

    There is another unfortunate regression: adding these theorems to the
    context prevents SMT solvers from giving `sat` answers. In fact, this
    happens even when just one theorem is added to the goal as an
    assumption (`integerTheory.INT`, specifically, which is needed to
    reason about `SUC`), regardless of which goal we try to prove.

    Fortunately, this does not prevent them from answering `unsat`.

    Since in the self-tests we do rely on `sat` answers to validate
    unprovable goals, the tests which expect a `sat` answer were modified
    to temporarily disable the inclusion of the above theorems while
    performing…
  • Loading branch information
@Plisp
Plisp committed Jun 12, 2024
1 parent 4e98178 commit 3b07de4
Show file tree
Hide file tree
Showing 1,187 changed files with 145,686 additions and 170,121 deletions.
56 changes: 50 additions & 6 deletions .github/workflows/docker-ci-for-pr.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,36 +11,80 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v3
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: false
build-args: |
SML=poly
Z3_VERSION=4.13.0
CVC_VERSION=5
BUILDOPTS=--stdknl -j2 -t
build-expk:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v3
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: false
build-args: |
SML=poly
Z3_VERSION=4.13.0
CVC_VERSION=5
BUILDOPTS=--expk -j2 -t
build-mosml:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: false
build-args: |
SML=mosml
BUILDOPTS=--expk --seq=tools/sequences/upto-parallel -t
build-otknl:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: false
build-args: |
SML=poly
Z3_VERSION=4.13.0
CVC_VERSION=5
BUILDOPTS=--otknl -j2 --seq=tools/sequences/upto-parallel
98 changes: 88 additions & 10 deletions .github/workflows/docker-ci.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,33 +15,35 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Docker meta
id: meta
uses: docker/metadata-action@v4
uses: docker/metadata-action@v5
with:
images: ${{ env.USERNAME }}/hol-dev
tags: |
type=sha,prefix=ci-,suffix=-stdknl
- name: Login to Docker Hub
uses: docker/login-action@v2
uses: docker/login-action@v3
with:
username: ${{ env.USERNAME }}
password: ${{ env.PASSWORD }}

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v3
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: true
build-args: |
SML=poly
Z3_VERSION=4.13.0
CVC_VERSION=5
# NOTE: the arg value cannot be quoted here:
BUILDOPTS=--stdknl -j2 -t
tags: ${{ steps.meta.outputs.tags }}
Expand All @@ -51,34 +53,110 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
uses: actions/checkout@v4

- name: Docker meta
id: meta
uses: docker/metadata-action@v4
uses: docker/metadata-action@v5
with:
images: ${{ env.USERNAME }}/hol-dev
tags: |
type=sha,prefix=ci-,suffix=-expk
- name: Login to Docker Hub
uses: docker/login-action@v2
uses: docker/login-action@v3
with:
username: ${{ env.USERNAME }}
password: ${{ env.PASSWORD }}

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v3
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: true
build-args: |
SML=poly
Z3_VERSION=4.13.0
CVC_VERSION=5
# NOTE: the arg value cannot be quoted here:
BUILDOPTS=--expk -j2 -t
tags: ${{ steps.meta.outputs.tags }}
labels: ${{ steps.meta.outputs.labels }}

build-mosml:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4

- name: Docker meta
id: meta
uses: docker/metadata-action@v5
with:
images: ${{ env.USERNAME }}/hol-dev
tags: |
type=sha,prefix=ci-,suffix=-mosml
- name: Login to Docker Hub
uses: docker/login-action@v3
with:
username: ${{ env.USERNAME }}
password: ${{ env.PASSWORD }}

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: true
build-args: |
SML=mosml
# NOTE: the arg value cannot be quoted here:
BUILDOPTS=--expk --seq=tools/sequences/upto-parallel -t
tags: ${{ steps.meta.outputs.tags }}
labels: ${{ steps.meta.outputs.labels }}

build-otknl:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4

- name: Docker meta
id: meta
uses: docker/metadata-action@v5
with:
images: ${{ env.USERNAME }}/hol-dev
tags: |
type=sha,prefix=ci-,suffix=-otknl
- name: Login to Docker Hub
uses: docker/login-action@v3
with:
username: ${{ env.USERNAME }}
password: ${{ env.PASSWORD }}

- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v3

- name: Build and push
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/Dockerfile
push: true
build-args: |
SML=poly
Z3_VERSION=4.13.0
CVC_VERSION=5
# NOTE: the arg value cannot be quoted here:
BUILDOPTS=--otknl -j2 --seq=tools/sequences/upto-parallel
tags: ${{ steps.meta.outputs.tags }}
labels: ${{ steps.meta.outputs.labels }}
45 changes: 37 additions & 8 deletions .github/workflows/self-runner.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ on:
kernel:
description: 'HOL kernel'
required: true
default: 'stdknl'
default: 'expk'
type: choice
options:
- stdknl
Expand All @@ -35,39 +35,65 @@ on:
more-options:
description: 'More options'
required: false
default: '-t'
type: string

Z3:
description: 'Z3 version'
required: false
default: '4.12.4'
type: choice
options:
- ''
- 2.19
- 2.19.1
- 4.12.4
CVC:
description: 'CVC version'
required: false
default: '5'
type: choice
options:
- ''
- 5
Yices:
description: 'Yices verison'
required: false
default: ''
type: choice
options:
- ''
- 1.0.40
jobs:
build:
runs-on: ubuntu-latest
steps:
-
name: Checkout
uses: actions/checkout@v3
uses: actions/checkout@v4
-
name: Set up QEMU
uses: docker/setup-qemu-action@v2
uses: docker/setup-qemu-action@v3
-
name: Docker meta
id: meta
uses: docker/metadata-action@v4
uses: docker/metadata-action@v5
with:
images: ${{ secrets.DOCKER_HUB_USERNAME }}/hol-dev
tags: |
# dynamically set the branch name as a prefix
type=sha,prefix={{branch}}-,suffix=-self
-
name: Login to Docker Hub
uses: docker/login-action@v2
uses: docker/login-action@v3
with:
username: ${{ secrets.DOCKER_HUB_USERNAME }}
password: ${{ secrets.DOCKER_HUB_ACCESS_TOKEN }}
-
name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2
uses: docker/setup-buildx-action@v3
-
name: Build and push
uses: docker/build-push-action@v3
uses: docker/build-push-action@v5
with:
context: .
file: developers/docker-ci/${{ env.default_dockerfile }}
Expand All @@ -76,6 +102,9 @@ jobs:
TARGETPLATFORM=${{ github.event.inputs.platform || env.default_platform }}
# NOTE: mosml is too slow to be chosen here
SML=poly
Z3_VERSION=${{ github.event.inputs.Z3 }}
CVC_VERSION=${{ github.event.inputs.CVC }}
YICES_VERSION=${{ github.event.inputs.Yices }}
# NOTE: the arg value cannot be quoted here:
BUILDOPTS=--${{ github.event.inputs.kernel || env.default_kernel }} -j${{ github.event.inputs.concurrency || env.default_concurrency }} ${{ github.event.inputs.more-options }}
tags: ${{ steps.meta.outputs.tags }}
Expand Down
32 changes: 0 additions & 32 deletions .travis.yml
View file

This file was deleted.

Loading

0 comments on commit 3b07de4

Please sign in to comment.