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

6404 commits

Author SHA1 Message Date
Leonardo de Moura
419100d42b feat: add Simp.Config.ground for simplifying nested ground terms 
This is an experimental new feature. We need more bells and whistles,
and `cbv` tactic for improving its performance.
 2023-10-19 13:59:17 -07:00
Scott Morrison
fb0d0245db
Revert "Cancel outstanding tasks on document edit in the language server" (#2703) 
* Revert "perf: inline `checkInterrupted`"

This reverts commit 6494af4513.

* Revert "fix: switch to C++ interruption whitelist"

This reverts commit 5aae74199b.

* Revert "fix: do not throw interrupt exceptions inside pure functions"

This reverts commit c0e3b9568e.

* Revert "feat: cancel tasks on document edit"

This reverts commit a2e2481c51.

* Revert "feat: translate `interrupted` kernel exception"

This reverts commit 14c640c15e.

* Revert "feat: check task cancellation in elaborator"

This reverts commit 2070df2328.

* Revert "feat: move `check_interrupted` from unused thread class to `Task` cancellation"

This reverts commit bf48a18cf9.
 2023-10-17 00:59:11 +00:00
Mario Carneiro
e0cba05167
refactor: env extensions can only modify .extensions (#2661) 2023-10-16 14:22:09 +11:00
Scott Morrison
1e74c6a348
feat: use nat_gcd in the kernel (#2533) 
* feat: use nat_gcd in the kernel

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-10-15 13:49:41 +11:00
Scott Morrison
66ab016723
chore: simp tracing reports ← (#2621) 
* chore: simp tracing reports ←

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
 2023-10-15 12:12:10 +11:00
Leonardo de Moura
b8af36fba0 chore: update comments at src/Lean/Meta/Basic.lean 
Co-authored-by: Timo <timorcb@gmail.com>
 2023-10-14 10:20:29 -07:00
Leonardo de Moura
29198371d9 chore: update comments at src/Lean/Meta/ExprDefEq.lean 
Co-authored-by: Timo <timorcb@gmail.com>
 2023-10-14 10:20:29 -07:00
Leonardo de Moura
3bc18797b0 fix: ensure transient cache results for different transparency modes don't mix up 2023-10-14 10:20:29 -07:00
Sebastian Ullrich
6d0a3287e0 fix: cache typos 2023-10-14 10:20:29 -07:00
Leonardo de Moura
e3b08060d0 fix: chore add workaround for corrupted cache 2023-10-14 10:20:29 -07:00
Leonardo de Moura
2253b788b4 perf: fine grain isDefEq cache for terms not containing metavariables 2023-10-14 10:20:29 -07:00
mhuisi
d0ae87d13f chore: improve error 2023-10-13 16:42:19 +02:00
mhuisi
b5348786a6 fix: pre-dependency-build-mode compatibility 2023-10-13 16:42:19 +02:00
mhuisi
253a5b931d fix: correct handling of FileWorker restarts 2023-10-13 16:42:19 +02:00
mhuisi
9945fa04d6 feat: FileWorker handling of --no-build 2023-10-13 16:42:19 +02:00
Sebastian Ullrich
4e1d95ce58 feat: pass along extra print-paths flags and handle no-build Lake error in server 2023-10-13 16:42:19 +02:00
Sebastian Ullrich
6494af4513 perf: inline checkInterrupted 
Amazingly, the extra result allocation seems to have triggered a mathlib
heartbeat timeout
 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
a2e2481c51 feat: cancel tasks on document edit 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
14c640c15e feat: translate interrupted kernel exception 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
2070df2328 feat: check task cancellation in elaborator 2023-10-13 09:52:26 +02:00
Scott Morrison
5d096c3fd8
chore: make Environment.add private (#2642) 
* feat: replay constants into an Environment

* suggestions from code review

* chore: make Environment.add private

* patch Lake to use Environment.add via extern
 2023-10-12 15:00:27 +11:00
Mario Carneiro
14e626a925 feat: ToMessageData (α × β) instance 2023-10-11 10:12:06 +02:00
Wojciech Nawrocki
856a9b5153 fix: treat pretty-printed names as strings 
I initially expected `Name`s to always faithfully represent internal data, in particular that a name with macro scopes would have a form such as  ```foo._@.Module._hyg.1``, and that tombstones would only appear in types that represent pretty-printed output such as as `String` or `Format`. However, that is not what happens. We have `sanitizeNames` which rewrites the `userName` field of local hypotheses to be `Name.str .anonymous "blah✝"`.

Then in the server code, we put these into `names : Array Name`e. This works fine for displaying in the infoview, but if we try to deserialize an `InteractiveHypothesisBundle` inside an RPC method for widget purposes, the `FromJson Name` instance blows up in `String.toName`.

I think my preferred solution is to, rather than 'fix' `String.toName` to accept these names with tombstones, stop pretending that they are actual `Name`s and re-type `InteractiveHypothesisBundle.names : Array String`. This should be a backwards-compatible change w.r.t. infoview code as the JSON representation is a string in either case. It is not backwards compatible w.r.t. meta code that uses this field.
 2023-10-11 09:51:14 +02:00
Mario Carneiro
115991066d
chore: remove unnecessary partial in ForEachExpr.visit (#2657) 2023-10-11 04:28:54 +00:00
Scott Morrison
076908d13b
feat: replay constants into an Environment (#2617) 
* feat: replay constants into an Environment
 2023-10-11 14:08:03 +11:00
Scott Morrison
ca0e6b0522
chore: fix MVarId.getType' (#2595) 
* chore: fix MVarId.getType'

* add test
 2023-10-09 11:04:33 +00:00
Sebastian Ullrich
00e981edcd perf: do not inhibit caching of default-level match reduction 2023-10-08 17:24:20 -07:00
Leonardo de Moura
9f50f44eed perf: missing cache at whnfImp 2023-10-08 17:22:14 -07:00
int-y1
8d7520b36f chore: fix typos in comments 2023-10-08 10:46:05 +02:00
David Christiansen
b0b922bae4 feat: list the valid case tags when the user writes an invalid one 
Before, Lean would simply emit the message "tag not found". With this
change, it also tells the user what they could have written that would
be accepted.
 2023-10-06 11:14:21 +02:00
David Christiansen
4c6d2b3998 doc: fix typo in comment 
Fix a misspelled/mistyped word in a comment.
 2023-10-06 11:14:21 +02:00
Mario Carneiro
89b65c8f1d
feat: make Environment.mk private (#2604) 
* feat: make `Environment.mk` private

---------
 2023-10-04 22:02:54 +11:00
kuruczgy
83c7c29075
fix: XML parsing bugs (#2601) 
* fix: make XML parser handle trailing whitespace in opening tags

* fix: make XML parser handle comments correctly

---------

Co-authored-by: György Kurucz <me@kuruczgy.com>
 2023-10-04 11:51:22 +11:00
Alex J Best
44bc68bdc6
fix: withLocation should use withMainContext for target (#2607) 2023-10-04 10:12:43 +11:00
Arthur Adjedj
6b93f05cd1
feat : derive DecidableEq for mutual inductives (#2591) 
* feat : derive `DecidableEq` for mutual inductives

* doc: document `RELEASES.md`

---------
 2023-10-03 02:17:13 +00:00
Denis Gorbachev
4b47462ccc refactor: remove redundant let 2023-10-02 14:27:04 +02:00
Denis Gorbachev
e6292bc0b8
doc: fix docstring typos (#2605) 
* lake: fix a typo in `get_config?` syntax doc
* fix a typo in `withImporting` doc
 2023-09-30 07:51:35 -04:00
Joachim Breitner
ae470e038e
docs: fix doc comment syntax in declModifiers doc comment (#2590) 
The hover on `declModifiers` says doc comments are `/-! … -/`, when it
should say `/-- … -/`.
 2023-09-27 11:57:40 +10:00
Mario Carneiro
e6fe3bee71 fix: hover term/tactic confusion 2023-09-26 10:16:37 +02:00
Sebastian Ullrich
83ecac4fd8 perf: lake: build lakefile environment incrementally 2023-09-22 22:01:07 +02:00
Arthur Adjedj
325fab1c1d
fix: don't try to generate below for nested predicates. (#2390) 
* fix: don't try to generate `below` for nested predicates.

* doc : document test #2389

* doc : document `mkBelow`

* test: extend `2389.lean`

* style: fix comments in `IndPredBelow.lean` and `2389.lean`
 2023-09-21 14:24:37 +10:00
thorimur
e79370a1e6
fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom (#2502) 
* fix: `withCollectingNewGoalsFrom`
do not collect old goals

* fix: update occurs check

* test: fix test `run/492.lean`

* docs: add docstring to `elabTermWithHoles`

* test: `refineFiltersOldMVars`

* test: fix `expected.out` name

* test: fix `expected.out` filename and line numbers

* docs: use long ascii dash instead of em dash

Co-authored-by: Scott Morrison <scott@tqft.net>

* docs: fix long line, mention lean4#2502

* docs: a couple more long lines

* test: fix line numbers

---------

Co-authored-by: Scott Morrison <scott@tqft.net>
 2023-09-21 14:23:27 +10:00
Sebastian Ullrich
dc60150b5a chore: update domain 2023-09-20 15:13:27 -07:00
Joachim Breitner
b2d668c340
perf: Use flat ByteArrays in Trie (#2529) 2023-09-20 13:22:37 +02:00
Patrick Massot
0a59fd96a5
chore: finer-grained ref in getCalcFirstStep (#2563) 
Suggested by @gebner at https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Random.20calc.20ranges/near/372704972
 2023-09-19 18:58:23 +00:00
Henrik
0d5f9122a1 perf: reduce allocations in unused variable linter 2023-09-18 05:41:37 -04:00
David Renshaw
ba416f2c1c fix: rename parameter of withImportModules to match doc string 2023-09-18 05:40:47 -04:00
Sebastian Ullrich
3e755dc0e1 fix: enforce linebreak between calc steps 2023-09-18 05:39:41 -04:00
thorimur
018020d36f
fix: uninterpolated error message in registerRpcProcedure (#2547) 2023-09-18 11:39:04 +02:00
Scott Morrison
c318d5817d feat: allow configuring occs in rw 2023-09-13 12:03:18 -07:00