This Github action automatically updates `stage0` on `master` if
`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h`
are out of sync there.
It bypasses the merge queue to be quick, this way, an out-of-date stage0
on on
master should only exist for a few minutes.
Needs access to a _deploy SSH key_ with write permission.
The elaborator is prone to duplicate terms, including recursive calls,
even if the user only wrote a single one. This duplication is wasteful
if we run the tactics on duplicated calls, and confusing in the output
of GuessLex. So prune the list of recursive calls, and remove those
where another call exists that has the same goal and context that is no
more specific.
Implements "gaps" in string literals. These are escape sequences of the
form `"\" newline whitespace+` that have the interpretation of an empty
string. For example,
```
"this is \
a string"
```
is equivalent to `"this is a string"`. These are modeled after string
continuations in
[Rust](https://doc.rust-lang.org/beta/reference/tokens.html#string-literals).
Implements RFC #2838
before code like
def dup (a : Nat) (b : Nat := a) := a + b
def rec : Nat → Nat
| 0 => 1
| n+1 => dup (dup (dup (rec n)))
decreasing_by decreasing_tactic
would run the `decreasing_tactic` 8 tims, because the recursive call
`rec n` gets duplicate due to the default paramter. Similar effects can
be observed due to dependent types or tactics like `cases`.
This is wasteful, and is confusing to the user when they use
`decreasing_by` interactively. Therfore, we now go through the proof
obligations (MVars) and if solving one would imply solving another one,
we assign the mvars to each other accordingly.
This PR is a sibling of #3004.
I found the documentation page hard to parse, so I figured I should fix
this. It's mostly indentation (e.g. in lists), some line breaks and
making URLs clickable.
With
set_option showInferredTerminationBy true
this prints a message like
Inferred termination argument:
termination_by
ackermann n m => (sizeOf n, sizeOf m)
it tries hard to use names that
* match the names that the user used, if present
* have no daggers (so that it can be copied)
* do not shadow each other
* do not shadow anything from the environment (just to be nice)
it does so by appending sufficient `'` to the name.
Some of the emitted `sizeOf` calls are unnecessary, but they are needed
sometimes with dependent parameters. A follow-up PR will not emit them
for non-dependent arguments, so that in most cases the output is pretty.
Somewhen down the road we also want a code action, maybe triggered by
`termination_by?`. This should come after #2921, as that simplifies that
feature (no need to merge termination arguments from different cliques
for example.)
by showing the matrix of calls and measures, and what we know about that
call (=, <, ≤, ?), e.g.
guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing
measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
x1 x2 x3
1) 29:6-25 = = =
2) 30:6-23 = ? <
3) 31:6-23 < _ _
Please use `termination_by` to specify a decreasing measure
It’s a bit more verbose for mutual functions.
It will use the user-specified argument names for functions written
```
foo (n : Nat) := …
```
but not with pattern matching like
```
foo : Nat → …
| n => …
```
This can be refined later and separately (and maybe right away in
`expandMatchAltsWhereDecls`).
This is pure refactoring: Instead of solving each subgoal as we
encounter it while traversing the syntax tree, we leave the `MVar`
there, at the end collect them all using `getMVarsNoDelayed`, and then
solve them.
This is a refactoring preparing for two upcoming changes:
* removing unexpected duplicate goals that can arise from term
duplication
* running interactive tactics on all, not each goal (#2921)
In order to not regress with error locations, we have to associated the
`TermElabM`’s syntax refernce with the `MVar` somehow. I do this using
the existing `mkRecAppWithSyntax` expression annotation, on the `MVar`’s
type. Alternatives would be stack another `StateT` on the traversal
and accumulate `Array (MVarId, Syntax)` explicitly, but that did not
seem to be more appealing.
This sets the build directory to `build/release` for the "CMake Tools
for Visual Studio Code" extension documented at
https://vector-of-bool.github.io/docs/vscode-cmake-tools/settings.html#cmake-builddirectory.
It also sets the generator to `make`, since otherwise it tries `Ninja`
which doesn't work.
Without these settings, the extension runs configure in a bad place at
startup.
This does *not* add the cmake tools extension to the default workspace
configuration; the goal is simply to prevent bad behavior for users who
already have the extension enabled.
# Summary
Screenshot of this in action:
Link to `RFC` or `bug` issue: N/A, this is not a bug nor a user-visible
feature.
Now that we're, at least temporarily, relying more on the Nix CI,
replace some old hacks of mine with better solutions people have figured
out in the meantime.
Cachix support could probably be dropped at this point but it doesn't
really hurt.
In order to familiarize myself with this code, and so that the next
person has an easier time, I
* added docstrings explaining what I found out these things to
* rewrote the syntax expansion functions using syntax pattern matches,
to the extend possible
else I see
```
[ 69%] Building CXX object runtime/CMakeFiles/leanrt.dir/platform.cpp.o
/home/jojo/build/lean/lean4/src/runtime/io.cpp:509:75: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64));
^
, ""
/home/jojo/build/lean/lean4/src/runtime/io.cpp:517:74: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64));
^
, ""
2 warnings generated.
```
when building
CI will now run on _any_ manually added label; hard to avoid.
Fun fact: Because the `toolchain-available` label is added by a github
action with the default token, it will _not_ trigger the workflow. Lucky
coincidence.
Following up on #2986, stop running the test suite in ci.yml in quick
mode; the test suite is run in the Nix job, and we do not need to run it
twice.
With a cold nix cache, when `lean` is rebuilt, not much changes, as both
jobs take ~20mins. But when `lean` is unchanged, the nix build should
be faster, and shaving off the (currently) 4mins in the CI.yaml run
should get us to a green PR sooner.
Another benefit is that we get the PR release sooner and even get it
when the test suite fails, which can be useful if you want to test
mathlib or other things before fixing the lean test suite.
which also removes an error condition at the use site.
While I am at it, I rename a parameter in `GuessLex` that I forgot to
rename earlier.
The effect will be user-visible (in obscure corner cases) with #2960, so
I’ll have the test there.
A few places would benefit from a `lambdaTelescopeBounded` that
garantees the result has the right length (eta-expanding when
necessary). I’ll look into that separately, and left TODOs here.
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
```
Now that there is a helpful message at the point of use when
`supportInterpreter` is required, we don't need to clutter every
`lakefile` with the advice.
there is a little dance with `if: success()` because otherwise a failed
`build` job would make this new job skipped, not failed, and I fear
skipped means ok when it is a required job.
So let’s make sure this job actually fails.
Also turn this into a proper check, run when a PR is opened or edited.
I took the liberty to rename the workflow file and name, so that one
doesn't have to look inside to guess what the workflow is doing.
If here is only one plausible measure, there is no point having the
`GuessLex` code see if it
is terminating, running all the tactics, only for the `MkFix` code then
run the tactics again.
So if there is only one plausible measure (non-mutual recursion with
only one varying
parameter), just use that measure.
Side benefit: If the function isn’t terminating, more detailed error
messages are shown
(failing proof goals), located at the recursive calls.
Removes the `CI` option from the `math` template. Since the template
does not currently generate a GitHub workflow, it does not do anything
out of the box except add unnecessary complexity.
The `math` template is also now tested in `tests/init` (minus the
Mathlib `require`).
