Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[WIP] LLVM Backend #1837

Merged
merged 51 commits into from
Dec 30, 2022
Merged

[WIP] LLVM Backend #1837

merged 51 commits into from
Dec 30, 2022

Commits on Dec 10, 2022

  1. Squashed commit of the following: 

    commit aef704da6ac84bb9f3eb2f8813820b8ae83d3b31
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Dec 10 14:16:58 2022 +0000

    Squashed commit of the following:

    commit 7034e64b4fcc0dada766c176d6aa748c71d05a50
    Author: Wojciech Nawrocki <wjnawrocki@protonmail.com>
    Date:   Thu Dec 8 13:21:37 2022 -0500

        doc: update widget example

    commit 57a6aefb924026d9a695dbf7fb53bf6603ad9733
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Thu Dec 8 15:55:40 2022 -0800

        chore: CI: also save core dumps for builds

    commit 43e3b78eb0efb7bd5b9e784e3a3665ddc8fd6818
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Wed Dec 7 11:58:12 2022 -0800

        feat: CI: capture core dumps

    commit a9ba08ce11ab9f257f9a0b8611944c53f4517b61
    Author: Wojciech Nawrocki <wjnawrocki@protonmail.com>
    Date:   Tue Dec 6 20:04:44 2022 -0500

        doc: document msgToInteractiveDiagnostic

    commit 6169435259e696a92209d56a8722b16c3f78579f
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Tue Dec 6 15:38:30 2022 +0100

        refactor: consolidate `MessageData` constructors into lazy formatting with infos

    commit 0b243f0ca33e1f6a2948c94896b22b2f304ac4c8
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Sun Nov 27 16:58:50 2022 +0100

        chore: Nix: avoid import errors for now

        Gotta refactor this anyway

    commit 9e83115072be337316d800febd298d99904d15d5
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Sun Nov 27 00:05:01 2022 +0100

        chore: Nix: lazy-trees compatibility

    commit 768ef310a016d8f4f99aa0f170bc43e18922ea38
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Sat Dec 3 15:04:05 2022 +0100

        refactor: Nix: LeanInk rendering based on packages, not directories

    commit ed3fa3734149f3375b2d15a8a544a7c55c2963dd
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Sat Dec 3 14:02:47 2022 +0100

        chore: Nix: add `overrideBuildModAttrs`

    commit 4b87103931af0fee4012bf31a30d757a2747583a
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Fri Dec 2 14:34:37 2022 -0800

        chore: ignore document version errors

    commit fe09c9c824a6b9c9499b1a3229830650c045b991
    Author: tydeu <tydeu@hatpress.net>
    Date:   Fri Dec 2 17:46:19 2022 -0500

        chore: update Lake

    commit e16880607800ed68a6e2c2a2aebf60d1b75227c9
    Author: ChrisHughes24 <chrishughes24@gmail.com>
    Date:   Fri Dec 2 12:41:45 2022 +0000

        chore: rename Prod.ext

    commit 8a573b5d87a42bd19307522ee747aaed44d9d71c
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Fri Dec 2 10:04:01 2022 -0800

        fix: fixes #1900

    commit a999015371adcc5516f2994b95251f312e3c820c
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Fri Dec 2 09:58:41 2022 -0800

        feat: add `applicationTime` to `registerTagAttribute`

    commit 50fc4a6ad84f215d9515e418d2770cab585f0254
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Fri Dec 2 08:57:37 2022 -0800

        fix: fixes #1907

    commit 681bbe5cf40ebd45019db2a84cd04dc0c63b8539
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Thu Dec 1 18:16:11 2022 -0800

        feat: ByteArray.hash

    commit a67a5080e95ba31cc72105bf0007f3c5113403a7
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Thu Dec 1 18:06:53 2022 -0800

        chore: fix tests after hash change

    commit c83e33b06a10103024151779424601a001640204
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Thu Dec 1 17:45:28 2022 -0800

        chore: update stage0

    commit 9b416667e7a8e8c36bc60c060479b1afb4218d8d
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Thu Dec 1 17:45:10 2022 -0800

        chore: replace all hashes by murmurhash

    commit b0cadbc1fa2e8080658f96f92595f034031ac984
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Tue Nov 29 17:15:17 2022 -0800

        fix: support escaped field names in deriving FromJson/ToJson

    commit 3d1571896c477bf06d709bd6d8a958529c22875b
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Tue Nov 29 17:14:52 2022 -0800

        fix: support escaped field names in dot-notation

    commit 7af80766e3ab1a676f05c31e0186d5f6bfabf62a
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Thu Dec 1 12:47:34 2022 -0800

        fix: do not ignore applicationTime in parametric attributes

    commit ffb0f42aae1e763196213b06e685ec30e4e02996
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Dec 1 08:39:06 2022 -0800

        fix: fixes #1901

    commit 0dda3a8c0258f0d40b1fa285258e67d5b27c1198
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Dec 1 06:11:48 2022 -0800

        fix: include instance implicits that depend on `outParams` at `outParamsPos`

        This fixes the fix for #1852

    commit 0a031fc9bbb43c274bb400f121b13711e803f56c
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Dec 1 05:17:23 2022 -0800

        chore: replace `Expr.forEach` with `Expr.forEachWhere`

    commit af5efe0b2d0837b9846a32b32c382d8135ddcd76
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Thu Dec 1 10:11:42 2022 +0100

        doc: `MonadReader`

    commit 50b2ad89b4721b0d011832207a6f5a95cc2c1717
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Thu Dec 1 10:06:32 2022 +0100

        test: limit maxRecDepth

    commit 30d625697e13bb23b6ad02aa49d16fe55fbe4bb7
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 18:44:20 2022 -0800

        chore: use `Expr.forEachWhere` to implement linter

        closes #1899

        TODO: use `Expr.forEachWhere` in other modules. There are many other opportunities.

    commit 1c5706bcc0bb822b306665efb07dfa6cfb1864b8
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 18:41:12 2022 -0800

        feat: add `Expr.forEachWhere`

    commit 5a151ca64cf18371455997fcb413d2513231d884
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 17:52:30 2022 -0800

        chore: fix tests

    commit 0db02c39118fc61facaf0ca90473b59eb14db080
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 16:59:08 2022 -0800

        chore: update Lake

    commit 95467dfab73c4a71a91ec2cf384276a42feb7042
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 16:11:05 2022 -0800

        chore: update stage0

    commit e5681ac141018e2fee4bcaf46b479e12900abecd
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 16:07:46 2022 -0800

        feat: replace `mixHash` implementation

        We are now using part of the murmur hash like Scala.
        For additional information and context, see
        https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-maintainers/topic/Increasing.20.60Expr.2Ehash.60.20to.2064.20bits/near/313114719

    commit 8fc3d77a0b01a654323d06f0dc1af1bc0572d06f
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 07:07:07 2022 -0800

        feat: add `trace.Meta.Tactic.simp.numSteps` and `trace.Meta.Tactic.simp.heads`

    commit 2a36cf42d2292a4ed867247df1d9ef10a741ae22
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 06:43:57 2022 -0800

        chore: update stage0

    commit aee63ee7b0a7ab41e285ad1f56e708da8337b7dc
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 06:39:49 2022 -0800

        feat: panic at `Name.append` if both names have macro scopes

    commit 7c5d91ebc3b82c6f73ca144960b31b3d47dd3765
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 30 06:31:03 2022 -0800

        fix: avoid `hygienic ++ hygienic` at `Specialize.lean`

    commit a095dabb17493f59695e04e7eaa95981b6d1b4f7
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Tue Nov 29 23:06:04 2022 -0800

        feat: `Name.append` and macro scopes

    commit bc21716bad4080240117d181cb259fff26ca181a
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Tue Nov 29 23:05:48 2022 -0800

        chore: helper `simp` theorems

    commit 3e45060dd52c13ee4904da1ccf6279df154f1a8a
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Tue Nov 29 14:12:07 2022 -0800

        fix: disable implicit lambdas for local variables without type information

        Problem reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/why.20doesn't.20this.20unify.3F/near/312806870

    commit 1b5029222859a52ad1afcd23f5fbfd64b047e17a
    Author: Scott Morrison <scott.morrison@gmail.com>
    Date:   Wed Nov 30 05:03:12 2022 +1100

        chore: protect Prod.Lex

    commit bc0684a29c72e40382d3b5b444c259acad057781
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Tue Nov 29 13:32:55 2022 +0100

        fix: work around VS Code completion bug

    commit 069873d8e5e0e7bed18f71edb63d18da50748ec9
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Tue Nov 29 08:57:56 2022 -0800

        fix: fixes #1891

    commit 40e212c166174d8cf81d874612c91c9e1d4023b2
    Author: Mario Carneiro <di.gama@gmail.com>
    Date:   Mon Nov 21 14:39:07 2022 -0500

        feat: infer def/theorem DefKind for `let rec`

    commit 6e23ced6d94ee71fafbf7986b63c98711aaaeb23
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Mon Nov 28 17:32:19 2022 -0800

        fix: test

    commit bdbab653fdccd1cf04a7af3ecb138a76daa914fb
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Mon Nov 28 14:29:17 2022 -0800

        fix: synthesize tc instances before propagating expected type

    commit 5286c2b5aa30403cbf75f9e67d406edbfca12b67
    Author: Henrik Böving <hargonix@gmail.com>
    Date:   Sun Nov 27 13:32:43 2022 +0100

        feat: optimize mul/div into shift operations

    commit 24cc6eae6d7231eb6c275970bfbb35a391577de6
    Author: Henrik Böving <hargonix@gmail.com>
    Date:   Sun Nov 27 13:32:29 2022 +0100

        feat: log2 for Fin and UInts

    commit a38bc0e6ed9e3318f882a5ee35c7d284d2fb3e42
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Sat Nov 26 13:12:40 2022 +0100

        refactor: revise server architecture

        Replace complex debouncing logic in watchdog with single `IO.sleep` in
        worker `didChange` handler, replace redundant header change logic in
        watchdog with special exit code from worker.

    commit 17ef0cea8a3c135b38a97bc028be846b27a14557
    Author: Mario Carneiro <di.gama@gmail.com>
    Date:   Tue Nov 22 00:31:15 2022 -0500

        feat: intra-line withPosition formatting

    commit 07953062ed590e58612bc0f85471cd926e7a33d4
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Mon Nov 14 13:34:24 2022 +0100

        perf: remove unnecessary, cache-defeating `withPosition` in `doReassignArrow`

    commit 9dbd9ec55433d50e19fba42756c242bee8d650a5
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Mon Nov 28 07:52:54 2022 -0800

        chore: fix build

    commit 6bc919742ebfa4a9fad9f2434ae984d012039473
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Mon Nov 28 07:51:42 2022 -0800

        chore: update stage0

    commit c510d16ef5e1e96fd6886450cd4549662d230ab2
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Mon Nov 28 07:47:32 2022 -0800

        fix: fixes #1808

    commit dfb5548cab54dfcf37cba5ec8c4e25fa305215e0
    Author: Siddharth Bhat <siddu.druid@gmail.com>
    Date:   Tue Nov 22 01:27:41 2022 +0000

        fix: update libleanrt.bc, rename to lean.h.bc

        This adds `lean.h.bc`, a LLVM bitcode file of the Lean
        runtime that is to be inlined. This is programatically generated.

        1. This differs from the previous `libleanrt.ll`, since it produces an
           LLVM bitcode file, versus a textual IR file. The bitcode file
           is faster to parse and build an in-memory LLVM module from.
        2. We build `lean.h.bc` by adding it as a target to `shell`,
           which ensures that it is always built.

        3. We eschew the need for:

        ```cpp
        ```

        which causes breakage in the build, since changing the meaning of
        `static` messes with definitions in the C++ headers.

        Instead, we build `lean.h.bc` by copying everything in
        `src/include/lean/lean.h`, renaming `inline` to
        `__attribute__(alwaysinline)` [which forces LLVM to generate
        `alwaysinline` annotations], then running the `-O3` pass pipeline
        to get reasonably optimised IR, and will be perfectly inlined
        when linked into the generated LLVM code by
        `src/Lean/Compiler/IR/EmitLLVM.lean`.

        Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

    commit a3dfa5516d3ba68358adcaf1063c35dd2764c75c
    Author: Scott Morrison <scott.morrison@gmail.com>
    Date:   Sun Nov 27 16:20:09 2022 +1100

        feat: add HashSet.insertMany

    commit 36cc7c23b6ade3ef787c1adbf8e1b6dbb08884de
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Mon Nov 28 06:14:19 2022 -0800

        fix: fixes #1886

    commit 092e26179bfb19790a63e5b9a260b089b1a286b3
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Mon Nov 28 15:47:17 2022 +0100

        chore: fix script/reformat.lean

    commit c112ae7c580832e3aa951ba2a40bb72fc19cae52
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Mon Nov 28 15:12:18 2022 +0100

        test: fix Lake rename

    commit c4ff5fe19914099dff571a4c74cc20f4247ab207
    Author: Scott Morrison <scott.morrison@gmail.com>
    Date:   Sun Nov 27 08:31:33 2022 +1100

        chore: change simp default to decide := false

    commit 42a080fae2ef6da9819e1dd998209b237c1042ed
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Fri Nov 25 10:31:01 2022 +0100

        fix: comments ending in `--/`

        Fixes #1883

    commit 39f2322f35f2b2eaadb5d62aad7f09796c1ef562
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Thu Nov 24 10:23:44 2022 +0100

        fix: save correct environment in info tree for `example`

    commit 543a7e26d492436b54d49b8796a054f79a3280db
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Nov 24 13:03:45 2022 -0800

        test: for #1878

        closes #1878

    commit 17855b6e90a441eb2d6995a126e10a65080a7ad7
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Nov 24 12:57:43 2022 -0800

        chore: update stage0

    commit 4be7543adbfb4805b980761182bde945aa3c67ae
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Nov 24 12:55:41 2022 -0800

        feat: add APIs for issue #1878

        We need `update-stage0` because this commit affects the .olean format.

    commit c53c5b5e16a11afeefd0a021773eabbde3742c7b
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Nov 24 12:33:39 2022 -0800

        fix: fixes #1882

        Better support for `intro <type-ascription>`.
        It was treating it as a pattern before this commit.

    commit 897ccd3783087682853a63255ea9c29033f4e9db
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Nov 24 12:33:21 2022 -0800

        chore: spaces

    commit 9d8b324f8dc9253da362d98220b07b209b8bfd26
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Nov 24 11:55:45 2022 -0800

        fix: fixes #1869

        Better support for simplifying class projections.

    commit 71b7562c2fb8c1dbefcca80ded29abb08442dae6
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Thu Nov 24 05:42:29 2022 -0800

        fix: class projection at `DiscrTree`

    commit 75f8ebdd199f181e8709c69d478d706b2c33fa26
    Author: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    Date:   Thu Nov 24 03:08:45 2022 +0000

        doc: update changelog

    commit 6225a3e41540dac592886acee6a8a719af3195ef
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Wed Nov 23 18:01:09 2022 -0800

        chore: update Lake

    commit 1ec535d5237e3eb8725285b07e26d686ace28090
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 23 18:45:17 2022 -0800

        test: alternative encoding experiment for `decEq` and `noConfusion`

    commit 1e79d659f25789b46b4d34f653d1317d816ba30a
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Wed Nov 23 10:17:21 2022 -0800

        chore: bundle libatomic in releases

    commit 06dc85453ed1e98a46b52124c997a8cc78a0a024
    Author: Gabriel Ebner <gebner@gebner.org>
    Date:   Wed Nov 23 10:07:13 2022 -0800

        chore: CI: allow releases not starting with v

    commit 9b572d4e2089a055b84dc0e55fa106cb87eac3d7
    Author: Mario Carneiro <di.gama@gmail.com>
    Date:   Tue Nov 22 21:30:01 2022 -0500

        chore: make `<;>` left associative

    commit 0694731af8c259972a35720db1ad6bbb67ad5fbe
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Wed Nov 23 05:42:20 2022 -0800

        fix: fixes #1870

    commit 9c561b593a70a5206e69bc31684f7d084aedc59b
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Tue Nov 22 14:27:35 2022 -0800

        feat: add `withTraceNodeBefore` and use it at `ExprDefEq`

        `withTraceNode` uses the metavariable context after executing
        `k`. This is bad when debugging `isDefEq`.

    commit dfaf9c6ebded4338e760963d1a13832d773bef50
    Author: Leonardo de Moura <leonardo@microsoft.com>
    Date:   Tue Nov 22 13:32:50 2022 -0800

        chore: register missing trace options, and fix `inherited` parameter

        The current setting was bad for debugging `isDefEq` issues.

    commit cbf7da0f6ef35774407132cf8f5802daf2c9a39b
    Author: Sebastian Ullrich <sebasti@nullri.ch>
    Date:   Tue Nov 22 17:43:55 2022 +0100

        chore: CI: update all actions to avoid warnings

commit 1322c488864975e92634c83463c3e044b4da37f2
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Dec 10 14:06:09 2022 +0000

    chore: fix merge conflict due to bootstrap.nix

commit 4279c0893ec6eefa490df88872d3b277ea8fdfd6
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Dec 10 13:09:14 2022 +0000

    fix: disable nix LLVM 15

commit 0cce49b216f75a4ea33022e1c463dd9840ca46d6
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Dec 10 11:19:30 2022 +0000

    chore: delete valgrind

commit 145026a02451e69e7b5f200ed1f754b2ff4ade91
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Dec 10 09:57:18 2022 +0000

    chore: resolve runtime CMakeLists.txt

commit 46296012e0b57d052875df2a33df220e92e51c05
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Dec 10 10:25:18 2022 +0000

    fix: add CMake to check for LLVM config version 15

commit cccc1796681844c5783faeeff4d8b3379781061e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Dec 9 18:36:29 2022 +0000

    fix: init

commit b87540389d5a4077ea1d3b0a1178a4aa2b9ec75f
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Dec 9 18:03:33 2022 +0000

    fix: float.lean

commit 5b64cdb9cd3857b21c5ac98af50ab0e582a95ac8
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Dec 9 15:32:09 2022 +0000

    [wip]: fix miscompile, now everything crashes at runtime

commit f202fae30e2eb96d3f0484ab45fd298433ad0d98
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Dec 9 09:50:04 2022 +0000

    fix: implement correct GEP for global string

commit 1767930b66a396764f8b21d9a48583662e9a2147
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Dec 9 09:20:51 2022 +0000

    fix: incorrect type signatures

commit 8c474b83e29a048685b139fc4ecacd4fa252a8b9
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Dec 9 09:04:31 2022 +0000

    fix: GEP -> load from global

commit 44d494d25933ceefbc5122a0f17345dff8c724b2
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Dec 9 08:37:32 2022 +0000

    fix: try to codegen pointer type, now headers are wrong

    It appears that it's unable to find the API 'LLVMPointerTypeInContext'
    which was added in LLVM 15?

commit e11cf04f4abe16c67f448c8b9b4a07d3b2051732
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Dec 8 17:34:08 2022 +0000

    fix: add debug logging for GEP

commit 7183d098e1860c1c7ba5e574a54ffb99c0c17eed
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Dec 8 15:26:41 2022 +0000

    fix: fixed buildCall, now fix GEP

commit 87bb27ad5a3fc8cc92f4f49ee6b538da8c5df24c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Dec 8 12:09:19 2022 +0000

    fix: switch over to call2/gep2/gep_inbounds2 API [WIP]

commit dd4f14f036e224c2bc2bb50579364764a894452c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Dec 8 11:29:03 2022 +0000

    fix: load -> load2

commit e42b0f5336efda75b529b95f2b002ef173741877
Author: Tobias Grosser <tobias@grosser.es>
Date:   Thu Dec 8 08:42:30 2022 +0000

    move LLVM stuff into leanshared

commit 59d80643cb85d4e0659c48e707ad440394f91e56
Author: Tobias Grosser <tobias@grosser.es>
Date:   Thu Dec 8 06:38:41 2022 +0000

    Install valgrind with sudo

commit 8af31f385cbc65091919309476154dfd581408c3
Author: Sebastian Ullrich <sebasti@nullri.ch>
Date:   Thu Dec 8 12:59:45 2022 +0100

    fix: copy `lean.h.bc` to stage 2 and beyond

commit 6b8f4b8581abf56d00c96d346643e4314155da81
Author: Sebastian Ullrich <sebasti@nullri.ch>
Date:   Thu Dec 8 11:55:36 2022 +0100

    fix: move `lean.h.bc` to a more appropriate place for distribution

    Fixes compilation with Nix

commit 8072584569c256fe8a05c600c0fbd2b30d6b5335
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Dec 8 06:02:32 2022 +0000

    fix: validate yaml

    I should give up pretending I know yaml syntax, I write it
    seldom enough that I always get it wrong on the first try.

commit e5defa04df17d6c477f0260f533ab96b8b0ef052
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Dec 8 05:31:43 2022 +0000

    chore: add Valgrind into CI and run LLVM backend

    Add a Valgrind profiled execution of lean compiling bitcode
    for expr.lean. This should help us figure out what the segfault
    on windows and linux release is.

commit 1e0edcf57beb7798003bf5cb282089b4e1a5b257
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Dec 7 17:02:57 2022 +0000

    fix: remove debug saving to /home/bollu/temp/

commit ce65981d4ba779d9636745291849ac520500409e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Dec 7 15:40:23 2022 +0000

    fix: remove debug code, run through valgrind to track what's happening?

commit 6449f26850a119264872a620508da14a0c9cd7b3
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sun Nov 27 22:25:27 2022 +0000

    fix: define forward declare in all settings

commit e64b0735cb8e42016f633deec04e5075608fcb4e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sun Nov 27 21:08:38 2022 +0000

    fix: remove failing test 'extern c inline'

    this is a stop-gap. Before the final merge, we should instead
    change the LLVM code generator to generate fallback code from
    the LLVM definition.

commit 3f81be1f6e6ff73441e6c37380115ea70ce73b66
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sun Nov 27 21:04:35 2022 +0000

    fix: remove references to llvm.o from ir.o

    - Before, `libleancpp.o` incurred a dependency on `LLVMBindings`.
      This is because `src/library/compiler/ir.cpp` invoked `lean_ir_emit_llvm`,
      which was defined in `libLean`, which needed `LLVMBindings` for the
      extern declarations.
    - By moving the use of `lean_ir_emit_llvm` directly into `shell.cpp`,
      this dependency was removed, allowing us to compile executables
      without incurring a dependency on all of LLVM.
    - TODO: check that this explanation makes sense by running it against
      @Kha. I'm not totally sure I get it just yet, I haven't had my morning
      coffee :)

commit 73366da822c0121cf79d8cd69d5ffccbcf3e629a
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 26 08:17:20 2022 +0000

    fix: remove llvm::initialize, move initialization into shell.cpp

commit 22ce4b2a7173b67259649627686c353011137006
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 26 07:53:42 2022 +0000

    Revert "fix: Give up and add LLVM flags to leanc as discussed with @gebner"

    This reverts commit 4ed112e493a6c728882e50ad8bf43f13bb5e15ff.

commit cb99b87ec2adedd5fe6e3b07c02a4f4ceb851f0e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 25 08:46:03 2022 +0000

    fix: remove dead import of LLVM in shell.cpp

commit 4ed112e493a6c728882e50ad8bf43f13bb5e15ff
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 25 08:09:25 2022 +0000

    fix: Give up and add LLVM flags to leanc as discussed with @gebner

    To test that this fixes the problem in one way, just add the LLVM
    link flags to `leanc`. This means that any executable build
    by lean that calls `open Lean` will now link against LLVM.

commit cb21c7b7b5ebaa3b20093d324761ed344b2eedeb
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 24 23:44:29 2022 +0000

    fix: set LLVM_DEBUG to 0 for shorter logs

commit 68a9ed6b402826e70827ef446f635560dc9a7495
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 24 22:28:53 2022 +0000

    fix: correctly do not include EmitLLVM

commit a021b1f9921d2bcf56b66690931dcbb4ee66c9e2
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 24 08:04:43 2022 +0000

    fix: remove 'extern c' from tests

    We cannot codegen 'extern c' with the LLVM backend. Remove
    uses of 'extern c'.

    This changes the value of computedFieldsExtern.

commit 659a3e78db89f4de01612530cc3a509857dd32e7
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 24 07:37:51 2022 +0000

    fix: change path to lean.h.bc

commit 00a5509b675bd1607b99df93ca11f6fa838dc872
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 24 03:24:53 2022 +0000

    fix: add -D LEAN_LLVM to CMAKE_CXX_FLAGS so it get passed to libleanshared correctly

commit 98208224f5cca23ff5da904649920a998fc3dd59
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 23 23:18:03 2022 +0000

    fix: 'tests/bench/compile.sh' should check for LLVM support

commit 58d10bd9622c275653241bcd750bf1b60c3b7df1
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 23 22:18:00 2022 +0000

    fix cmake

commit 7989e9ec5267c8e6196958b8a3b6ca9e4cd10fb4
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 23 04:50:50 2022 +0000

    fix: compile_lean -> compile_lean_{c,llvm}_backend

commit e28f908d8909b8b6d3d86bb0da6a58dfa8251d26
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Tue Nov 22 01:27:41 2022 +0000

    fix: update libleanrt.bc, rename to lean.h.bc

    This adds `lean.h.bc`, a LLVM bitcode file of the Lean
    runtime that is to be inlined. This is programatically generated.

    1. This differs from the previous `libleanrt.ll`, since it produces an
       LLVM bitcode file, versus a textual IR file. The bitcode file
       is faster to parse and build an in-memory LLVM module from.
    2. We build `lean.h.bc` by adding it as a target to `shell`,
       which ensures that it is always built.

    3. We eschew the need for:

    ```cpp
    ```

    which causes breakage in the build, since changing the meaning of
    `static` messes with definitions in the C++ headers.

    Instead, we build `lean.h.bc` by copying everything in
    `src/include/lean/lean.h`, renaming `inline` to
    `__attribute__(alwaysinline)` [which forces LLVM to generate
    `alwaysinline` annotations], then running the `-O3` pass pipeline
    to get reasonably optimised IR, and will be perfectly inlined
    when linked into the generated LLVM code by
    `src/Lean/Compiler/IR/EmitLLVM.lean`.

    Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

commit 1193b49edf7f1797f3abcf389bdd1fc7da62b41c
Merge: a6fed4bbfb 89e1bc72ed
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Tue Nov 22 20:23:32 2022 +0000

    Merge remote-tracking branch 'upstream/master' into nov-15-llvm-backend

    Perform this as a merge, since rebasing over these many commits
    is far too painful.

commit a6fed4bbfb54aa294b7b94faf3920b95134bbc9c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 03:19:28 2022 +0000

    fix: don't leak module/targetmachine

commit c3b96e5e3ddf7f9bacd766581b7eb26b9896ea10
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 02:57:24 2022 +0000

    beef up .gitignore

commit 98a4a1562efe89d2c03e6a7ab830f5f72a56f496
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 02:57:13 2022 +0000

    fix: remove janky debugging reset/reuse hack

commit a2f65e43ff08808d02459668504d8660b9deba48
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 02:09:45 2022 +0000

    fix: delete unused files

commit b53b8f1ac51021f2c5aa3a62e6bfbe5521069008
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 02:07:05 2022 +0000

    fix: space between LEAN_LLVM option

commit 49b67fcd88b63b9cf4fa8945303881a11381d58d
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 01:38:17 2022 +0000

    fix: run pass pipeline to optimise LLVM.

commit 278a779b1d784bbd7564467ccb0292562581a5b9
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 19:22:04 2022 +0000

    fix: LLVM initialization code outside ifdef

commit 8a813260631bf4216d5a2e765a46b2755f39acc8
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 06:17:36 2022 +0000

    fix: generate always_inline

commit 2e8b9111eb928a6cfc685441c16a65b2dc71d8d6
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 06:15:51 2022 +0000

    chore: add TODO for always_inline

commit 7f23776b4aa265fb0e712f8d168324dcf6b86f35
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 05:54:45 2022 +0000

    fix: make compativle with LLVM bindings

commit 3ea992c477988ab1a1da0ea88d618d7785019193
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 03:12:58 2022 +0000

    fix: Try to hide EmitLLVM from Lean.Compiler.IR

    Unfortunately, at least locally, I seem to still get the link
    errors:

    ---
    5/8 Test #1444: leancomptest_phashmap.lean ...............***Failed   10.04 sec
    running C program...
    rm: cannot remove './phashmap.lean.out': No such file or directory
    phashmap.lean:53:10: warning: unused variable `xs` [linter.unusedVariables]
    /usr/bin/ld: /home/bollu/work/lean-llvm/lean4/build/stage1/lib/lean/libleancpp.a(llvm.cpp.o): in function `array_ref_to_ArrayLLVMType(lean::array_ref<lean_object*> const&)':
    /home/bollu/work/lean-llvm/lean4/src/library/compiler/llvm.cpp:162: undefined reference to `LLVMPrintTypeToString'
    ...
    ---

commit 4b83fa4efa001a6a42add46372fff0d013b79ff2
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 03:00:28 2022 +0000

    fix: generate lean_inlines programatically

    Using `#define static extern` caused lots of crazy
    stuff to break in the header files. Instead, write a script
    that copies `src/include/lean.h`, and then uses `sed` to replace
    `static inline` in a controlled fashion. This ensures that the resulting
    `.ll` file has all the definitions we want.

commit 13c853dbf9edd57114a3f4f34d0aeafd8a7a0c5f
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 17 02:12:53 2022 +0000

    Revert "fix: use lean_inlines created by manually inlining things into a single file"

    This reverts commit 43cfe33104c788874e222ed73751734c8e6ab76e.

commit dcf9afa2377e361f6985facd922eebcd9fd6cd84
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 17 01:43:11 2022 +0000

    fix: produce bitcode directly from clang

    No need to produce LLVM and then round trip though opt
    to produce bitcode.

commit 22837856d1d526f8fbd4967f83adb263c1ce77eb
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 17 01:35:27 2022 +0000

    fix: produce bitcode, not textual IR

commit 4f8f37e1deee750b468e7fac0354eb8c9be9e1de
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Nov 17 01:27:14 2022 +0000

    fix: bring back include of EmitLLVM to ensure initialize is called.

    We need to have EmitLLVM in the import tree so that it is
    initialized correctly. Alternatively, we need to initialize
    it from the C++ side of things.

commit de48f3d5bf7a7455d63215a2a2b7bd175982af10
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 23:39:10 2022 +0000

    fix: fix script that runs LLVM backend

commit 121ac814ab4235852470723b238e75ca77b47ffb
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 23:07:53 2022 +0000

    fix: do not export EmitLLVM

commit a979664874d4343a27e68bd7c87bdead1f41cda4
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 22:52:47 2022 +0000

    chore: fix syntax highlight

commit a49e964d10b654d7f732afda8c76c9a5024f008a
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 22:38:18 2022 +0000

    fix: use lean_inlines created by manually inlining things into a single file

    I want to see if this fixes the totally mysterious error where clang
    starts picking up GCC headers:

    ---
    In file included from /home/bollu/work/lean-llvm/lean4/src/runtime/lean_inlines.cpp:3:
    In file included from /home/bollu/work/lean-llvm/lean4/build/stage1/include/lean/lean.h:14:
    In file included from /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/atomic:41:
    In file included from /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/bits/atomic_base.h:38:
    In file included from /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/bits/move.h:57:
    /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/type_traits:64:7: error: storage class specified for a member declaration
          static constexpr _Tp                  value = __v;
          ^
    ---

commit cd18cfeca3c2894d62d3cf80c1bf24d9adba5504
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 19:43:56 2022 +0000

    fix: change CMAKE_CXX_FLAGS less agressively for libleanshared.so

commit b8571c2f5d1ad9466e191b0309b7dc649ccd1ffa
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 19:42:05 2022 +0000

    fix: error: invalid argument '-std=c++14' not allowed with 'C'

    We continue to have errors, as locally, my config
    seems to pickup GCC headers instead of clang, leading to entertaining
    errors such as:

    ------
    In file included from /home/bollu/work/lean-llvm/lean4/src/runtime/lean_inlines.cpp:3:
    In file included from /home/bollu/work/lean-llvm/lean4/build/stage1/include/lean/lean.h:14:
    In file included from /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/atomic:41:
    In file included from /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/bits/atomic_base.h:38:
    In file included from /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/bits/move.h:57:
    /usr/bin/../lib64/gcc/x86_64-pc-linux-gnu/12.2.0/../../../../include/c++/12.2.0/type_traits:64:7: error: storage class specified for a member declaration
          static constexpr _Tp                  value = __v;
          ^
    -----

    It is unclear to me how this is happening.

commit e4cef282e067d31d1f9e7cc0f5a94119f6abd36c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 19:14:05 2022 +0000

    fix: add lean_has_llvm_support to query LLVM

commit 87b42dba93b811dbea07bf6bdf2210b46a1cc473
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 19:13:15 2022 +0000

    fix: only build libruntime_bc when LLVM is asked

    fixes make[5]: *** No rule to make target 'shell/runtime_bc', needed by 'shell/CMakeFiles/lean'.  Stop.

commit 7f732c3d658331185377e9fdce7b9e6cef161be9
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 18:17:47 2022 +0000

    fix: add libleanrt to shell build

    We need `libleanrt` to provide us a runtime when emitting code.
    This allows us to correctly build the runtime, and error out politely,
    at the location of the mismatch, if we can't access clang as the C++
    compiler.

    There used to be a global requirement that the LLVM backend needed
    clang, which I removed as legacy. I now see why it was potentially
    required (to build `libleanrt.bc`). Hopefully, placing the check
    for Clang and the erroring out here makes it clearer to the next person
    as to why we enforce the need for Clang when building the LLVM backend.

commit a84e101a08fe37019027ae5c7c6266ec4bbb19d9
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 10:19:07 2022 +0000

    add LLVM backend

commit e498b2d1c4f8ab9fa9a23417a1a7f333220af307
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 03:19:01 2022 +0000

    fix: add module and target machine freeing API

commit d4b1e88e72673200cdc8fcbf865c1bcc1469c3ce
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 01:54:15 2022 +0000

    fix: actually remove @&

commit 613a06d1b2e2923c14be5da76143a2ac9220685f
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Nov 19 01:27:36 2022 +0000

    fix: (1) nonempty, (2) ctx param, (3) remove &@, (4) PassManager.

    Fixes as suggested by @Kha, @gebner.
    Also add FFI bindings for `PassManager` and `PassManagerBuilder`.

commit 71da58332981364d41c0a89961e4949bbdc42dee
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 06:37:40 2022 +0000

    fix: IO -> BaseIO, inhabited instances.

commit c7d367926b6b85cdfcddb2060834d3bb18f6f853
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 05:55:25 2022 +0000

    fix: fixup API with enums

commit 7ae1cef14ec6584fb9fd6ee1fd6e30156be50388
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 03:58:09 2022 +0000

    chore: add spaces between structure defns

commit 5ee799061e33c3d3e2a64cffd378c0f0ce078f7c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 03:57:57 2022 +0000

    fix: change namespace+def enums to structures

commit 576783af33b466f5226c87732dabb5d25fbf7814
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 18 03:46:05 2022 +0000

    fix: use suggested structure API suggested by @Kha, @gebner

    We now use

    structure Foo (ctx: Context) where
      private mk ::
      ptr : USize

    Also fix the whitespace issue --  'f(var: T)' → 'f (var : T)'

commit c76215116987dba4750a3b37376cc14dcda9d9fa
Author: Siddharth <siddu.druid@gmail.com>
Date:   Thu Nov 17 18:29:15 2022 -0800

    Update src/Lean/Compiler/IR/LLVMBindings.lean

    Co-authored-by: Gabriel Ebner <gebner@gebner.org>

commit da409b2f8fed9c827fc69a5aaa617ec08d79317d
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 22:47:03 2022 +0000

    fix: log levels - llvm-config:status leanshared:verbose

    This should provide enough info about 'leanshared' cration
    when we want it warranted, while always printing out key things like
    LLVM config and LLVM flags that's super duper useful to view
    at a glance.

commit 8631ae86e14ab73dbb0219fbcd2404c439034514
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 22:44:00 2022 +0000

    chore: {True,False} -> const{True,False}

    This reduces ambiguity and making casing consistent.

commit e53f1b5a2949843c0cf577f647e3c8ec14ead48f
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 22:41:30 2022 +0000

    fix: LLVM_DEBUG -> 0

    This was changed in building the uber large LLVM
    backend patch on accident.

commit c3cbab99382f47c706425f8a349f33faa69c86d4
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 20:27:58 2022 +0000

    chore: make llvm-config logs live in 'verbose'

commit 8c27a01f27a7f7108d0d3e65222f963ad28e3f1d
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 20:26:02 2022 +0000

    chore: delete unused types

commit 4f09453a3234ab3e16ff237d266dbe537e9f267e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 16 10:17:46 2022 +0000

    update API as per @Kha suggestions

commit 8a08623694a9bf7ead66e704ea6ca9217376eef6
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 4 20:43:39 2022 +0000

    fix: assert -> static_assert, llvm file cleanup

commit 41a4f3d7b63a4c08373c9e35a9bba37f22dfbab8
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 4 20:33:29 2022 +0000

    fix: remove -DCMAKE_CXX_COMPILER_ID stage0 workaround

commit cf0486768fa2c017c72b8907207813a2653cd964
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 4 20:32:20 2022 +0000

    remove debug logging of leanc --print-{c,ld}flags

commit f659b9f5a62d1ae379fcd80d19538147c64e7f7b
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 4 20:31:10 2022 +0000

    fix: indentation of if(LLVM)

commit 5449f89c515de985bc94793730f9df7f11f4618e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 4 20:30:47 2022 +0000

    chore: remove comment about -DBUILD_SHARED_LIBS

commit 65e75df2fc7eb369ac8a3976d9e83f4980a1f73a
Author: Siddharth <siddu.druid@gmail.com>
Date:   Fri Nov 4 13:26:47 2022 -0700

    Update src/CMakeLists.txt

    Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

commit 040a6684aeda7480a06baaac98b4e29d0901203c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Nov 4 13:30:59 2022 +0000

    Revert "fix: simulate update-stage0 by updating stage0/src/CmakeLists.txt"

    Now that we no longer forward arguments from `stage1`
    to `stage0`, this ought to be un-necesssary as pointed out
    by @Kha.

    This reverts commit e0ae06420e4278141298be04d90f14292a4b8519.

commit e2bdd00c9086f58e5040920f3814784bc25f5d28
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 23:07:12 2022 +0000

    fix: typo

commit 607942e8f0271df4d1630b9157c633520b94546c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 17:02:36 2022 +0000

    fix: more descriptive error for llvm-config execution failure

    On macOS aarch64, before @Kha fixed the release:

    > CMake Error at CMakeLists.txt:263 (execute_process):
    >   execute_process error getting child return code: No such file or directory

    This error is generated by trying to run `${LLVM_CONFIG}`.

    This commit should also act as a 'bump' against the build,
    and this build should pass, since the macOS aarch64 build
    now succeeds on Lean HEAD: https://github.com/leanprover/lean4/pull/1795

commit 3134e5c55d714151927fd16a6c7e61fe8dab8d63
Author: Sebastian Ullrich <sebasti@nullri.ch>
Date:   Wed Nov 2 17:01:25 2022 +0100

    chore: Nix: clean up LLVM integration

commit 4d983c15d5313ea87736ece9ca25c1655f56f87e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 15:35:08 2022 +0000

    fix: remove size_tType

    As @tobiasgrosser said:

    > Why exactly is this hard-coded as 64 bit? Llvm does not even have a
    > size_t type. I am surprised the api offers such magic type interface. I
    > would maybe drop this for now and add it when actually needed. I
    > personally would probably put this type selection further out in the
    > backend or maybe just call it differently. This functionality really is
    > more about the c implementation on a given platform than about llvm.

commit acbb958f2857dd9060eaf1840b41d0f0efc03ed7
Author: Siddharth <siddu.druid@gmail.com>
Date:   Wed Nov 2 15:31:49 2022 +0000

    fix: llvm -> llvm-host in macos setup

    This mimics what we do in prepare-llvm-linux.sh to allow successful cross compiles.

    Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

commit a69e99da3b8496aa24d8c22f15109876f6f65bdb
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 14:21:56 2022 +0000

    chore: cleanup src/library/compiler/llvm.cpp

commit 986e6e51a07de94b559d47c32490840e3cff4e99
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 14:14:28 2022 +0000

    fix: cleanup CMakeLists

commit e78e7d366b3c7a9041ce4a6a58a9d9ada2ab91b4
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 14:13:25 2022 +0000

    fix: add -DLLVM=ON to nix

commit f0ade0d9ff60941a182e54e52d1acf362711a5ff
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 13:50:48 2022 +0000

    fix: remove nix overapproximation.

commit cf6af3316d8af156ce5e29c74e0374442b73d66f
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 13:40:35 2022 +0000

    fix: don't copy LLVM includes

commit 91ec7ad31b7db17e9811850a0e33e9991e39e6b8
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 10:01:15 2022 +0000

    fix: revert option forwarding, suggested by @Kha

    I don't fully understand the build process, but if I understand
    it correctly, then this ensures that we don't accidentally ask
    stage0 to build LLVM.

commit e0ae06420e4278141298be04d90f14292a4b8519
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 03:34:31 2022 +0000

    fix: simulate update-stage0 by updating stage0/src/CmakeLists.txt

    -DLLVM=ON means different things to old stage0 and new cmake script.

    To new cmake configuration, it means *don't* link in LLVM for stage0.
    to old cmake script, it mean *do* link in LLVM always.

    This leads to some kind of weird impedance mismatch between old/new?
    I am unclear on how precisely the `src/CMakeLists.txt` and
    `stage0/src/CmakeLists.txt` actually interact.

commit d1670a3974563e0c3a4c0258de9251699c3ec602
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Tue Nov 1 16:12:39 2022 +0000

    fix: add ifdef guard for llvm.cpp

commit 204a7ad37c26b72beaf800d1321266281ea6d916
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 03:18:39 2022 +0000

    fix: remove leftover  GREATER 0

commit 62f071a008006b0000a52b98b1f9d4e57d56fbc3
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Nov 2 01:38:58 2022 +0000

    fix: workaround staging; explicitly pass -DCMAKE_CXX_COMPILER_ID

    Because `stage0` has a different `CMakeLists.txt`, we get the error:

    > CMake Error at CMakeLists.txt:162 (message):
    >   LLVM=ON must be used with clang.  Set `CMAKE_CXX_COMPILER` and
    >   `CMAKE_C_COMPILER` accordingly.
    >

     We fix this by manually setting:

     > -DCMAKE_CXX_COMPILER_ID=Clang -DCMAKE_C_COMPILER_ID=Clang

     This can be removed once we update the stage0 build scripts.

commit 446103d77449584c53ae0624e0d903449a31d24a
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Tue Nov 1 11:00:53 2022 +0000

    fix: -DLLVM=OFF by default

commit f4e454f0f79107bec97aa0346bffa7dc7c2b2dde
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 31 19:51:40 2022 +0000

    fix: forward -DLLVM=ON

commit 716759a3c76266ceaa220107694599cb79164fe6
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 31 17:41:11 2022 +0000

    fix: remove stage>0 restriction

commit 32cae3a34ff0dafcb2414dda7ed585bcf3ce8340
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 31 00:32:53 2022 +0000

    fix: create list of forwarded options

commit ec0df3287e35c852e8f90556e4812de83ae68b96
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 31 00:29:01 2022 +0000

    fix: bring back LEAN_LLVM flag

commit 0fd6716e48758126466b53048951fc60811a3314
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 31 00:25:23 2022 +0000

    add stage0 checks more consistently

commit e2b9c37eee96b632830660cf4bd0cb6cff4eaf4c
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sun Oct 30 17:27:40 2022 +0000

    fix: fix nix-build test by adding llvm dependencies.

    Run nix build $NIX_BUILD_ARGS .#test -o push-test

commit 86a2cf2a807f2d764f24a714cdf4ae183d63ffcd
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Oct 26 12:15:01 2022 +0100

    fix: link against LLVM at stage > 0

commit a1d8f4fdc94d528292ccd120332698c35e263f33
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Tue Oct 25 14:36:02 2022 +0100

    fix: Get nix shell to work

    It appears that the `leanshared` nix target does not automatically link
    against LLVM. fix this by adding the appropriate LLVM calls.

commit d8a07b604ff1825ce95b4e818f1025f4331d522f
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 24 17:25:55 2022 +0100

    fix: add || true to print leanc flags

    Run lean-*/bin/leanc --print-cflags
    + lean-4.0.0-linux_aarch64/bin/leanc --print-cflags
    /home/runner/work/_temp/c5e995cd-aa15-4a4a-a4d9-e97601ae4409: line 1: lean-4.0.0-linux_aarch64/bin/leanc: cannot execute binary file: Exec format error

    See that the other option
      Run lean-*/bin/* || true

    also skips this on `aarch64`

commit cc73ffdf53a777f5c74717bacbc3c6987db1987a
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 24 16:52:22 2022 +0100

    fix: super janky, 's/llvm-host/llvm'

    This should fix the path issues we have. Currently,
    `llvm-config` spits out paths like:

    > 2022-10-24T14:21:30.1620266Z TODO: change to debug
    > llvm-config: libdir '/home/runner/work/lean4/lean4/build/llvm-host/lib'
    > ldflags '-L/home/ runner/work/lean4/lean4/build/llvm-host/lib'
    > cxxflags: -I/home/runner/work/lean4/lean4/build/llvm-host/
    > includedir: /home/runner/work/lean4/lean4/build/llvm-host/include

commit 175a92978de948db5dec28081bd6948f288e8266
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 24 15:10:30 2022 +0100

    fix: remove LEAN_EXTRA_LINKER_FLAGS

commit 51aeab9560fe509a0701861bbb2e85c370c96f6e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 24 14:19:13 2022 +0100

    fix: add LLVM flags to LEAN_EXTRA_LINK_FLAGS

commit 023c320869961ae4945ca8c818b91f357eaf1c71
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sun Oct 23 11:44:49 2022 +0100

    fix: change nix build inputs to over-approximation

    For whatever reason, nix believes the llvm-config is that of llvm-11:

commit d1fccb777ad5b58322ccba3fa0a5c8e03a414dc3
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sun Oct 23 11:37:18 2022 +0100

    chore: typos in cmakee, print leanshared flags.

    Debugging why we are unable to find LLVM symbols:

    2022-10-20T00:51:35.0046819Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld:
       /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so:
       undefined reference to `LLVMGetTargetFromTriple'
    2022-10-20T00:51:35.0047692Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld:
       /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so:
       undefined reference to `LLVMLinkModules2'
    2022-10-20T00:51:35.0049782Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld:
       /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so:
       undefined reference to `LLVMGetBasicBlockParent'
    2022-10-20T00:51:35.0052435Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld:
       /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so:
       undefined reference to `LLVMGetDefaultTargetTriple'

commit 3aec9301e6b4f28b2c68191987cc311e56900fc6
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Oct 20 00:58:47 2022 +0100

    fix: ${LLVM_CONFIG_LIBDIR } → ${LLVM_CONFIG_LIBDIR} (no ' ')

    This is the last commit before I go to bed, I promise. I hope
    that adding the path to where we ought to pick up the libraries
    will allow us to link against the right libraries.

commit 1311ba93570a1e4bac4ff82342db2a2ff2336685
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Oct 20 00:53:06 2022 +0100

    fix: add LLVM library path to -L...

commit 5ee7ebc5338394315efce817e13ef2870e22b59e
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Oct 20 00:42:45 2022 +0100

    Revert "fix: copy `llvm-host/llvm-config` to `stage1/`"

    This reverts commit 3f969ba5a6a835ef1ac306125320f1e2a5943c92.

commit 017472a5eb7655f715faabc563233e39cafc7ad5
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Oct 20 00:26:04 2022 +0100

    fix: nix: llvmPackages → llvmPackages_14

commit 3f969ba5a6a835ef1ac306125320f1e2a5943c92
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Thu Oct 20 00:24:47 2022 +0100

    fix: copy `llvm-host/llvm-config` to `stage1/`

    This should cause `llvm-config` to spit out the correct paths
    for includes, libs, etc. This is also very jank, since we
    are copying the *host* `llvm-config` into the *target release*
    directory. This is OK for testing, but we need to fix this
    hack, or do something else before release.

commit ea32631e096e8937ec59f8e1bd4a5f92accab013
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Wed Oct 19 22:39:53 2022 +0100

    fix: bintools for llvm-config on nix.

commit 7260ff0ddaab0cde858e30f0a54a63f9f839aa21
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 17 15:30:20 2022 +0100

    only link against LLVM for leanshared, lean

commit aba67a9fc932808cc9fbcfa9dadb9c0d28eb3789
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 17 14:15:27 2022 +0100

    fix: llvm libs path in the install tree

    See that the LLVM libs are copied to 'ROOT/lib/', not
    to `ROOT/llvm/lib/'.

    + tree --du -h lean-4.0.0-linux
    + grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
    ├── [8.9K]  LICENSE
    ├── [ 67K]  LICENSES
    ├── [8.0M]  bin
    ...
    ├── [ 46M]  include
    ...
    ├── [837M]  lib (@@@@@@@@)
    ...
    │   ├── [712M]  lean
    ...
    │   │   ├── [5.5M]  libInit.a
    │   │   ├── [ 79M]  libLean.a
    │   │   ├── [5.6M]  libleancpp.a
    │   │   ├── [632K]  libleanrt.a
    │   │   └── [ 61M]  libleanshared.so
    │   ├── [  13]  libLLVM-15.0.1.so -> libLLVM-15.so
    │   ├── [ 59M]  libLLVM-15.so (@@@@@@@@)
    │   ├── [  13]  libLLVM.so -> libLLVM-15.so
    ...

commit d576391d6c1c614a4bd495acb548207d21002194
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 17 13:26:45 2022 +0100

    fix: add " -L ROOT/llvm/lib" to Leanc linker flags

    We see that on the build runner, we get the flags:

    + lean-4.0.0-linux/bin/leanc --print-ldflags
    -I /home/runner/work/lean4/lean4/lean-4.0.0-linux/include -fPIC -fvisibility=hidden -L /home/runner/work/lean4/lean4/lean-4.0.0-linux/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -L/home/runner/work/lean4/lean4/build/llvm/lib -lLLVM-15 -lm -Wl,--as-needed -lgmp -Wl,--no-as-needed -ldl -pthread

    See that we have -L:
    1. /home/runner/work/lean4/lean4/build/llvm/lib
    2. /home/runner/work/lean4/lean4/lean-4.0.0-linux/lib/lean

    The path (1) is generated by
    `llvm-config`, relative to its location. It's also completely bunk.
    If we want to generate
    a sensible path from `llvm-config`, we should keep `llvm-config` within the `stage1/bin`
    tree, and then query `stage1/bin/llvm-config --libs` or whatever.

    Alternatively, We add another path like (2), expect to point to:
    /home/runner/work/lean4/lean4/lean-4.0.0-linux/lib/llvm/

    which will give it access to the LLVM libs.

    This commit attempts to perform solution (2), which adds a new path.
    I am not a CMake expert, so this might take a couple tries to get right.

commit 68f36b8ac920bac747acad1b960976090a1600e0
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Mon Oct 17 12:17:41 2022 +0100

    chore: print leanc --print-cflags, --print-ldflags

    I feel that previously, the paths were working out due
    to dumb luck, or me manually setting up LD_LIBRARY_PATH
    in the install script.

    Locally, 'leanc --print-ldflags' prints out:

    ```
    sirpinski :: lean-llvm/lean4 » leanc --print-ldflags
    -I /home/bollu/.elan/toolchains/leanprover--lean4---nightly/include -fPIC -fvisibility=hidden -L /home/bollu/.elan/toolchains/leanprover--lean4---nightly/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lm -Wl,--as-needed -lgmp -Wl,--no-as-needed -ldl -pthread
    ```

    Note that we only have
    `-L /home/bollu/.elan/toolchains/leanprover--lean4---nightly/lib/lean`

    I would have to either (a) move the `llvm-15.so` into `lib/lean`,
    or (b) add a linker path to the parent directory of `-L /home/bollu/.elan/toolchains/leanprover--lean4---nightly/lib`
    for it to pick up LLVM.

    Let's actually test this by looking at what
    `leanc --print-{cflags,ldflags} ` produces.

commit f5e0bfbaa26dc1a8746f1a83162d3190a7b3c73a
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 22:29:24 2022 +0100

    fix: think through how llvm-config should be used.

    How did this stuff ever work on linux?
    I need to run `llvm-target/bin/llvm-config` to find out the linker
    options I need for the target LLVM? But the target `llvm-config`
    is an `aarch64` binary, which we definitely can't run on the host
    `x86_64` machine!

    Do we take on faith that `llvm-host/bin/llvm-config` will provide
    flags that are approximately correct, and move ahead with that?
    That seems like a dubious assumption to me.

    It seems like it used to work on linux, as I had missed the
    `-DLLVM_CONFIG=path/to/llvm-config` option in the linux builds.
    So it was (luckily) finding the (host?) `llvm-config` and configuring
    itself correctly?

commit 722e958f030f5b6d61a5361a6c9c0f7d64f0a03d
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 20:29:17 2022 +0100

    fix: windows build '$CP' -> cp

    The windows build does not define a '$CP' variable, so switch
    to plain old 'cp'.

commit 252af0e1505d0cd6168cf914a89c4f34a76fe849
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 17:33:28 2022 +0100

    fix: ' ' when appending to LEANC_STATIC_LINKER_FLAGS

    This fixed the CI error on Linux Release:

    ld.lld: error: unknown argument '-Bdynamic-L/home/runner/work/lean4/lean4/build/llvm/lib'
    ld.lld: error: unable to find library -lLLVM-15

commit 132ebf4510d8b093d851bf612282ae7f0245c2b3
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 12:59:07 2022 +0100

    fix: revive LLVM headers copying to 'stage1/'

commit 0fe4062773c272dc2907f0a3057aeeacb650e712
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 12:48:50 2022 +0100

    fix: don't ship 'llvm-config'.

    We can use 'llvm-config' during build time and bake
    in the flags. There is no need to ship 'llvm-config'
    with 'stage1/bin'.

commit a3f3a7725c44354b5a871c54b1e58e62ed390a62
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 12:46:04 2022 +0100

    fix: add back 'llvm-config' copy+setup

commit fa4f62990dfa1f642ed2bc68c997f54604965fff
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 11:52:33 2022 +0100

    fix: bring back zlib for darwin

commit c45b2e8f61f2c2b34b817b3dde084ad9d65199c0
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Sat Oct 15 11:49:19 2022 +0100

    chore: cleanup cmake

commit fda1894920017ff723ed8a1924077b2b1594a9b5
Author: Siddharth Bhat <siddu.druid@gmail.com>
Date:   Fri Oct 14 17:36:42 2022 +0100

    Squashed commit of the following:

    link to zlib correctly on macos

    Thanks to @tobiasgrosser:
    https://github.com/tobiasgrosser/lean4/pull/6/files#diff-148715d6ea0c0ea0a346af3f6bd610d010d490eca35ac6a9b408748f7ca9e3f4

    add LLVM bindings
    link against LLVM via llvm-config
    @bollu
    bollu committed Dec 10, 2022
    Configuration menu
    Copy the full SHA
    07d2fae View commit details
    Browse the repository at this point in the history

  2. fix: remove runtime_bc that accidentally got added by merge

    @bollu
    bollu committed Dec 10, 2022
    Configuration menu
    Copy the full SHA
    e48c62a View commit details
    Browse the repository at this point in the history

  3. fix: delete logging code

    @bollu
    bollu committed Dec 10, 2022
    Configuration menu
    Copy the full SHA
    99453b3 View commit details
    Browse the repository at this point in the history

Commits on Dec 11, 2022

  1. fix: remove debugging shell code; [[ -v ]] does not exist on macos bash 

    https://stackoverflow.com/a/669486
    @bollu
    bollu committed Dec 11, 2022
    Configuration menu
    Copy the full SHA
    3e66564 View commit details
    Browse the repository at this point in the history

  2. fix: move lean.h.bc to a more appropriate place for distribution 

    Fixes compilation with Nix
    @Kha @bollu
    Kha authored and bollu committed Dec 11, 2022
    Configuration menu
    Copy the full SHA
    1c4c666 View commit details
    Browse the repository at this point in the history

  3. chore: print lean.h.bc path to see what's going wrong in Windows

    @bollu
    bollu committed Dec 11, 2022
    Configuration menu
    Copy the full SHA
    a9c3366 View commit details
    Browse the repository at this point in the history

  4. fix: add check for LLVM before stage2 copying of resources

    @bollu
    bollu committed Dec 11, 2022
    Configuration menu
    Copy the full SHA
    e6cc2cd View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2022

  1. fix: change CMAKE_LIBRARY_OUTPUT_DIRECTORY -> CMAKE_ARCHIVE_OUTPUT_DI… 

    …RECTORY

on windows, CMAKE_LIBRARY_OUTPUT_DIRECTORY is the same as `bin/`, as DLLs
must live next to `exe`s. Thus, we use `CMAKE_ARCHIVE_OUTPUT_DIRECTORY` to
refer to the underlying `lib/` folder on Windows. This allows us to
correctly store `lean.h.bc` at the right path. (`/lib/lean.h.bc`).

given infinite time, someday, considering generating these paths
from the `CMake` into a autogenerated `Lean.Compiler.HardcodedPaths' file,
and all shall be solved without hardcoded path duplication.
    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    ec745f0 View commit details
    Browse the repository at this point in the history

  2. chore: delete extraneous newline

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    a14efcf View commit details
    Browse the repository at this point in the history

  3. fix: remove extraneous whitespace

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    6258c32 View commit details
    Browse the repository at this point in the history

  4. chore: cleanup

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    583d0ba View commit details
    Browse the repository at this point in the history

  5. chore: remove dead code in shell.cpp

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    d24f00e View commit details
    Browse the repository at this point in the history

  6. fix: remove newline before EOF at tests/bench/.gitignore

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    53ede98 View commit details
    Browse the repository at this point in the history

  7. chore: remove dead cmake code

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    4260455 View commit details
    Browse the repository at this point in the history

  8. fix: undo accidental :wq change to tests/common.sh

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    de67bef View commit details
    Browse the repository at this point in the history

  9. chore: undo moving Context after BB in LLVMBindings.lean

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    25ddb32 View commit details
    Browse the repository at this point in the history

  10. fix: remove stale TODO about refcounts

    @bollu
    bollu committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    5372358 View commit details
    Browse the repository at this point in the history

Commits on Dec 13, 2022

  1. chore: cleanup file

    @bollu
    bollu committed Dec 13, 2022
    Configuration menu
    Copy the full SHA
    eec52bc View commit details
    Browse the repository at this point in the history

  2. chore: cleanup of functions

    @bollu
    bollu committed Dec 13, 2022
    Configuration menu
    Copy the full SHA
    c46768a View commit details
    Browse the repository at this point in the history

  3. chore: kill multi newline

    @bollu
    bollu committed Dec 13, 2022
    Configuration menu
    Copy the full SHA
    75cee18 View commit details
    Browse the repository at this point in the history

  4. chore: callLeanMainFn

    @bollu
    bollu committed Dec 13, 2022
    Configuration menu
    Copy the full SHA
    ef83b3f View commit details
    Browse the repository at this point in the history

  5. chore: lean_initialize

    @bollu
    bollu committed Dec 13, 2022
    Configuration menu
    Copy the full SHA
    1e0ff69 View commit details
    Browse the repository at this point in the history

  6. chore: modInit

    @bollu
    bollu committed Dec 13, 2022
    Configuration menu
    Copy the full SHA
    8c62091 View commit details
    Browse the repository at this point in the history

Commits on Dec 15, 2022

  1. chore: fix (val:ty) to (val : ty)

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    0670111 View commit details
    Browse the repository at this point in the history

  2. chore: fix some (let _ <- ...) by changing types

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    f14596a View commit details
    Browse the repository at this point in the history

  3. chore: allow default (name : String := ) consistently

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    0245157 View commit details
    Browse the repository at this point in the history

  4. chore: reuse code to emit modInitFn

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    e01cd87 View commit details
    Browse the repository at this point in the history

  5. chore: refactor PureDeclInitFn

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    12595fe View commit details
    Browse the repository at this point in the history

  6. chore: remove dead comments/code

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    863923d View commit details
    Browse the repository at this point in the history

  7. chore: more minor nit squashing

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    86fda94 View commit details
    Browse the repository at this point in the history

  8. chore: prettify commits, remove dead TODOs

    @bollu
    bollu committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    ab4b84e View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2022

  1. Update src/Lean/Compiler/IR/LLVMBindings.lean 

    Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
    @bollu @Kha
    bollu and Kha committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    eaa7b85 View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2022

  1. fix: remove spurious -DCMAKE_CXX_FLAGS in CMake

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    bf37bb6 View commit details
    Browse the repository at this point in the history

  2. fix: Eliminate inductive error type.

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    4de7d9c View commit details
    Browse the repository at this point in the history

  3. fix: eliminate eprintln

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    e2f1dd2 View commit details
    Browse the repository at this point in the history

  4. fix: main type is voidPtrType

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    ed351c2 View commit details
    Browse the repository at this point in the history

  5. Revert "fix: undo accidental :wq change to tests/common.sh" 

    Sadly, I had forgotten why I had changed 'tests/common.sh'.
The old version of 'tests/common.sh' had 'diff_produced' exit on
success. I had changed it to continue on success.

Unfortunately, I got mixed up during review, and thought this was a
typo. Revert the change, and fix the bugs that I've definitely
introduced in the process!

This reverts commit de67bef.
    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    33f8ed7 View commit details
    Browse the repository at this point in the history

  6. fix: modInit needs a module name, there was an extra init being appended

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    2a43323 View commit details
    Browse the repository at this point in the history

  7. fix: remove _ match in Decl

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    9ae78f5 View commit details
    Browse the repository at this point in the history

  8. fix: /- should be /-- for doc comments

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    171a446 View commit details
    Browse the repository at this point in the history

  9. fix: StateT -> StateRefT

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    35cd76f View commit details
    Browse the repository at this point in the history

  10. fix: remove pointer cast as they're a thing of the past

    @bollu
    bollu committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    7a9c829 View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2022

  1. chore: remove semicolons

    @bollu
    bollu committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    08a0806 View commit details
    Browse the repository at this point in the history

  2. chore: fixups of TODOs and alignment

    @bollu
    bollu committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    2325a9e View commit details
    Browse the repository at this point in the history

  3. chore: hanging args are double indented

    @bollu
    bollu committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    422e53f View commit details
    Browse the repository at this point in the history

  4. fix: implement Data.HashMap.mkIdx in extern C 

    Since the LLVM backend cannot use inline C code,
we move the inline C code to an extern definition
in `lean.h`. This ensures we do not regress in performance,
while allowing the LLVM backend to compile tests that use
`Data.HashMap`.
    @bollu
    bollu committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    eb44554 View commit details
    Browse the repository at this point in the history

  5. chore: fix indent, use consume_io_result

    @bollu
    bollu committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    2367b17 View commit details
    Browse the repository at this point in the history

  6. chore: fix gitignore

    @bollu
    bollu committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    8dbdfb9 View commit details
    Browse the repository at this point in the history

Commits on Dec 20, 2022

  1. fix: make test scripts consistent 

    The scripts `tests/{compiler,bench}/test_single.sh` run the C
and LLVM backends. We make them consistent:

- print "running LLVM" in both scripts.
- delete out `.out` file in both scripts.
- add comment describing C and LLVM backends in both scripts.
    @bollu
    bollu committed Dec 20, 2022
    Configuration menu
    Copy the full SHA
    00bbafa View commit details
    Browse the repository at this point in the history

  2. fix: delete computedFieldsExtern test case 

    Nuke the test case, since the entire point of the test
was to check for `extern c inline`, which no longer works
with the LLVM backend.

Perhaps we ought to find some way to selectively turn off the LLVM
backend on a test.
    @bollu
    bollu committed Dec 20, 2022
    Configuration menu
    Copy the full SHA
    0cd1291 View commit details
    Browse the repository at this point in the history

  3. fix: nuke lean_inlines.cpp 

    We build `lean_inlines` differently now, by building
the bitcode file directly from the header file via
`sed` magic, thus the `lean_inlines.cpp` is no longer
necessary.
    @bollu
    bollu committed Dec 20, 2022
    Configuration menu
    Copy the full SHA
    10afa9b View commit details
    Browse the repository at this point in the history