max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
31930 commits 1 branch 0 tags 5.3 GiB
Commit graph

31930 commits

This branch
This branch
All branches
Author SHA1 Message Date
Joachim Breitner
fbefbce8c7
doc: Adjust contributor's docs to squash merging (#2927) 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-11-21 10:13:43 +00:00
Scott Morrison
f1b274279b
feat: helpful error message about supportInterpreter (#2912) 
Following [@Kha's
suggestion](https://github.com/leanprover/lean4/issues/2897#issuecomment-1816043031)
from #2897.

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
 2023-11-21 10:31:26 +01:00
Kyle Miller
6a33afb745
feat: Lean.MVarId.cleanup configuration (#2919) 
Modifies `cleanup` so that it takes (1) an array of additional fvarids
to preserve and (2) a flag to control whether to include indirect
propositions.

(This is wanted in mathlib for the `extract_goal` tactic.)
 2023-11-21 10:09:48 +01:00
Joachim Breitner
9800e066bc
fix: PackMutual: Deal with extra arguments (#2892) 
previously, it would ignore a recursive call that has extra arguments,
which can happen when the recursive functions return something of
function type. Therefore just leave them extra arguments in place.

Fixes #2883.
 2023-11-20 17:07:50 +01:00
Mac Malone
5858549037
doc: release notes for recent lake fixes 
Co-authored-by: Scott Morrison <scott@tqft.net>
 2023-11-20 15:51:31 +00:00
Kyle Miller
4d39a0b0e3
fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument (#2918) 
Fixes #2914
 2023-11-20 20:51:47 +11:00
Sebastian Ullrich
9bf0f5116b
chore: more code owners 2023-11-20 09:30:18 +01:00
Scott Morrison
8b86beeb07 doc: clarify doc-string for Lean.Elab.Tactic.withLocation (#2909) 
In the previous doc-string, the sentence

> "If any of the selected tactic applications fail, it will call
`failed` with the main goal mvar."

was false both for `Location.wildcard` (where it should have said "If
all", not "If any") or for `Location.targets` (where `failed` is never
called).
 2023-11-20 09:15:27 +01:00
Mario Carneiro
8881517018 fix: report goals in induction with parse error 2023-11-20 09:15:27 +01:00
Eric Wieser
0668544a35 feat: add an OfNat instance for Level (#2880) 
This allows writing `1 : Level`, which is pretty handy for using `Sort 1` aka `Type`.

Co-authored-by: Scott Morrison <scott@tqft.net>
 2023-11-20 09:14:16 +01:00
Marcus Rossel
1362268472
doc: fix typos (#2915) 2023-11-19 20:00:47 +00:00
tydeu
65d08fdcdd chore: ignore forgotten Lake test artifacts 2023-11-17 21:25:41 -05:00
tydeu
e29c3239e3 fix: lake: whitelist loaded config olean env exts 2023-11-17 13:50:14 -05:00
Adrien Champion
ed1a98d5ae
doc: add documentation for universe, open, export, variable 
Add documentation comments with examples to `universe`, `open`,
`export`, and `variable`.

The documentation shows up when hovering over keywords, hopefully
improving the experience for beginners.
 2023-11-17 13:19:10 +00:00
github-actions[bot]
c6e4b98793 doc: update changelog 2023-11-17 12:32:02 +00:00
Leni Aniva
ab36ed477e
feat: allow trailing comma in tuples, lists, and tactics (#2643) 2023-11-17 13:31:41 +01:00
tydeu
5d1d493635 feat: bare lake init & validated pkg names 2023-11-16 12:54:52 -05:00
Mac Malone
893d480c77
refactor: lake: use plain lib name for root and native name 2023-11-16 12:49:46 -05:00
tydeu
857ba0a3e5 fix: support non-identifier library names 2023-11-16 12:48:55 -05:00
Joachim Breitner
ad77e7e762
chore: Issue template: Suggest #eval Lean.versionString (#2884) 
as this works also on https://live.lean-lang.org/ or for people
not familiar with the command line.
 2023-11-16 18:40:55 +01:00
Scott Morrison
b3e9bb4997 chore: update release notes after v4.3.0-rc2 2023-11-16 21:55:25 +11:00
Sebastian Ullrich
139973217c
chore: more code owners 2023-11-16 10:09:54 +01:00
tydeu
b770060b9e doc: lakefile.olean compatibility check release note 2023-11-15 19:31:08 -05:00
tydeu
8a2054ca09 fix: stricter lakefile.olean compatibility check 2023-11-15 19:31:08 -05:00
tydeu
171837216a feat: IO.FS.Handle.lock/tryLock/unlock 2023-11-15 19:31:08 -05:00
tydeu
19c81a19ea feat: IO.FS.Handle.rewind/truncate 2023-11-15 19:31:08 -05:00
Sebastian Ullrich
7cc2c9f1c9
doc: code owners (#2875) 2023-11-15 18:21:23 +01:00
Alexander Bentkamp
7fb7b5c5cb
chore: releases for web assembly and x86 Linux (#2855) 2023-11-15 18:18:47 +01:00
tydeu
bbc759522a doc: lake: flexible manifest release notes 2023-11-15 00:39:06 -05:00
tydeu
712d3c2292 chore: deprecate Lake.PackageConfig.manifestFile 2023-11-15 00:39:06 -05:00
tydeu
73540ecd48 feat: lake: use / in Windows manifest file paths 2023-11-15 00:39:06 -05:00
tydeu
d07e8fd6a4 test: lake: add manifest version upgrade test 2023-11-15 00:39:06 -05:00
tydeu
446d547817 refactor: lake: more flexible manifest 2023-11-15 00:39:06 -05:00
Scott Morrison
37c2ec10e9 chore: fix conditional syntax in pre-release.yml 2023-11-15 12:24:20 +11:00
Eric Wieser
6f2eb3f6b4 doc: fix typo 2023-11-15 12:19:42 +11:00
Kyle Miller
76a7754d08 fix: have parenthesizer copy source info to parenthesized term 
This causes the info view to have the entire parenthesized expression be hoverable.
 2023-11-14 20:24:30 +01:00
Sebastian Ullrich
77ee031172 fix: re-read HTTP header when skipping notification in Ipc.readResponseAs 2023-11-14 17:34:04 +01:00
Sebastian Ullrich
2f35651308 perf: leak environments not freed before process exit 2023-11-14 17:33:04 +01:00
Sebastian Ullrich
62dc8d7308 feat: Runtime.markMultiThreaded/Persistent 2023-11-14 17:33:04 +01:00
tydeu
6d349201b4 doc: add note on .lake to RELEASES.md 2023-11-13 20:31:24 -05:00
tydeu
dcb92296f6 test: use built lake for examples/reverse-ffi 2023-11-13 20:31:24 -05:00
tydeu
4ec3d78afa chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
tydeu
2ff4821026 refactor: .lake directory for Lake outputs 2023-11-13 20:31:24 -05:00
tydeu
ffd79a0824 fix: lake: ensure untar output directory exists 2023-11-13 20:31:24 -05:00
Sebastian Ullrich
8cfcf7ce61 fix: look through binop% variants in elabCDotFunctionAlias? 2023-11-12 16:57:51 +11:00
Sebastian Ullrich
dbe1c7f459 fix: make ^ a right action, add NatPow and HomogeneousPow 2023-11-12 16:57:51 +11:00
Kyle Miller
4bd0525a99 chore: update stage0 2023-11-12 16:57:51 +11:00
Sebastian Ullrich
31f234ba3c feat: leftact%/rightact% binop variants 2023-11-12 16:57:51 +11:00
Kyle Miller
262f213391 chore: update stage0 2023-11-12 16:57:51 +11:00
Sebastian Ullrich
8b145b05e2 feat: add leftact%/rightact% syntax 2023-11-12 16:57:51 +11:00