max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
31966 commits 1 branch 0 tags 5.3 GiB
Find a file
Joachim Breitner 367ac01279
chore: trim CI set by default (#2986) 
The goal of this change is to run a trimmed-down CI on PRs by default,
but allows opt-in the full CI as necessary.

### Specification

The CI workflow runs in “quick” mode if it was triggered from a pull
request, and that pull request does not have the `full-ci` label set.

In “quick” mode the build matrix contains fewer jobs. At the moment
only:

* Linux-release, to get the PR releases.

In non-quick mode everything should be as before.

### Implementation notes

I created a `configure` job that combines all the previous `set-` jobs,
I guess this is faster than firing up separate jobs.

The matrix is calculated in this job; this seems to be the cleanest way
to get a dynamic matrix going (experiments using `exclude` failed). The
downside is that the matrix is now in JSON rather than Yaml syntax. The
upside is that we can (later) make it’s calculation simpler, e.g. set
default `shell` values etc.

I was not able to make it so that CI runs when the `full-ci` label is
added, but don’t do anything otherwise. I think it can be done with
another workflow listening to `labeled` and then triggering this one,
but let’s do that separately. For now, add the label and then push (or
close and reopen).

The checks
```
  if: matrix.build-stage2 || matrix.check-stage3
  if: matrix.check-stage3
```
were dead code, we did not have these fields in the matrix anymore, so I
replaced them with
```
  if: matrix.test-speedcenter
```
2023-11-29 13:24:45 +00:00
.github chore: trim CI set by default (#2986) 2023-11-29 13:24:45 +00:00
.vscode doc: fix some syntax and link in the docs, and more 2021-10-10 11:36:43 +02:00
doc doc: Adjust contributor's docs to squash merging (#2927) 2023-11-21 10:13:43 +00:00
images
nix feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
script chore: script/most-recent-nightly-tag uses https rather than ssh repo URL (#2951) 2023-11-23 10:27:46 +00:00
src doc: Improve docstrings around Array.mk,.data,.toList (#2771) 2023-11-29 08:49:13 +00:00
stage0 feat: embed and check githash in .olean (#2766) 2023-11-27 10:24:43 +00:00
tests feat: WF.GuessLex: If there is only one plausible measure, use it (#2954) 2023-11-27 22:41:40 +00:00
.gitattributes chore: Do not hide stage0/src/stdlib_flags.h from diffs 2023-09-13 19:29:25 +02:00
.gitignore chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
.ignore chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
CMakeLists.txt feat: embed and check githash in .olean (#2766) 2023-11-27 10:24:43 +00:00
CODEOWNERS chore: more code owners 2023-11-20 09:30:18 +01:00
CONTRIBUTING.md doc: Adjust contributor's docs to squash merging (#2927) 2023-11-21 10:13:43 +00:00
default.nix doc: setup 2021-01-03 13:21:58 +01:00
flake.lock chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00
flake.nix chore: Nix: use strings instead of URL literals (#2172) 2023-03-28 10:10:24 +02:00
LICENSE chore: remove LICENSE header that confused GitHub 2021-11-18 09:42:35 +01:00
LICENSES chore: add GMP license for now 2021-11-18 09:42:35 +01:00
README.md doc: Update contribution guides (#2624) 2023-10-25 13:05:55 +11:00
RELEASES.md doc: release notes for recent lake changes (#2938) 2023-11-27 18:30:45 +00:00
shell.nix chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00

README.md

This is the repository for Lean 4.

We provide nightly releases and have just begun regular stable point releases.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.