nightly-2021-07-25

Changes since nightly-2021-07-24:

Full commit log

• 60e6130 chore: Nix: expose benchmarks as flake attributes for convenience
• 43190e0 feat: FromToJson for recursive inductives
• 4073b20 chore: add bcrypt in CMakeLists
• f7f0064 chore: update stage0
• d6893a3 fix: more robust LspEncoding
• 75feb9c chore: fix type and add copyright
• 2f828ee chore: update stage0
• 54f2769 fix: test
• f27a069 chore: drop UntypedRef and use monotonic RpcRefs
• 66258b0 chore: fix windows build
• 102236f chore: leftover comment
• ffc6efd fix: use properly random RPC session id
• 776a0c7 feat: add UInt64 unpackings
• b3d9e90 feat: IO.getRandomBytes
• 9a5cdaf chore: address review 1
• ef34cfd chore: more extensive LspEncoding test
• cfb5d34 fix: parser arity
• 9664fc8 chore: add test
• 3accff6 feat: deriving LspEncoding handler
• f077dd0 feat: RPC ref decrement
• 85dcdcd chore: use NonScalar
• 80d9003 feat: add Format tags
• 1b42255 feat: check RPC reference types
• 4a93c9a chore: purify WorkerM
• d97e1b9 chore: drop RPC wrappers for now
• b3316fd feat: RPC handlers
• f891279 chore: drop one namespace
• 4d83e79 feat: more RPC handlers
• 3ec568c feat: initial RPC
• 2e6382e feat: untyped references
• 079c290 feat: JSON serde for Name and USize
• d716bf0 fix: preserve lifted CoreM traces
• 4a3c172 feat: parametrised deriving handlers

nightly-2021-07-24

Changes since nightly-2021-07-23:

Full commit log

• 1b12884 chore: fix test
• 3d402ed chore: missing !
• 57b4b8a chore: disable the kernel "tryHeuristic" for abbreviations
• cce6165 perf: refine tryHeuristic
• 0d9c5f5 chore: use zeta expansion at AbstractNestedProofs module
• 1630cd3 chore: missing argument

nightly-2021-07-23

Changes since nightly-2021-07-22:

Full commit log

• 1eee82f fix: Windows build
• 9ff8e3e chore: remove obsolete C++ tests
• 2b451a3 chore: remove obsolete serializer code
• 5b1cfc2 chore: remove obsolete header
• dc3d94f fix: check arity in notation unexpander
• 98634b5 fix: $(_):ident is not an infallible pattern
• 5866e2b chore: use register_parser_alias where possible
• 42e681a fix: make unterminated comments consume all input

nightly-2021-07-22

Changes since nightly-2021-07-21:

Full commit log

• a6af257 fix: missing condition
• c5ffcc5 refactor: remove redundant condition

nightly-2021-07-21

Changes since nightly-2021-07-20:

Full commit log

• 0943dc3 chore: update stage0
• a019d80 chore: document simplified object header and remove obsolete cmake options
• 10122ba chore: try to fix compilation error at CI
• 286136b fix: missing std::
• fa8b842 chore: update stage0
• c59e72a chore: cleaner lean_dec_ref, inline persistent object case
• da66610 chore: cleanup
• 974caa9 chore: typo
• e0132ea chore: update stage0
• 489b280 feat: simpler and faster RC

nightly-2021-07-20

Changes since nightly-2021-07-17:

Full commit log

• 7e317d2 feat: term info on where declarations
• b76dd1a feat: go-to-definition for local variables
• df57b43 fix: go-to-type on parameterized types
• 18becc7 fix: plain term goal on binders
• 4a4b4c1 fix: mkAtomFrom: generate synthetic position like other *From functions
• 904cfd6 perf: extract cold path in lean_alloc_small
• 16fbbf9 perf: extract cold paths in lean_free_small and mark noinline
• 52810bd chore: remove dead header
• 8637220 fix: make precedence mandatory for mixfix commands
• caa8f7f chore: expose Substring.prev/next
• f07e49a chore: parse names properly
• 55a506b chore: adapt test
• 03699cd feat: uniformly split idents
• 7aca461 fix: hovers on elabFieldName fields
• bcde967 feat: add dot hover test
• b2d712a fix: Substring.splitOn

nightly-2021-07-17

Changes since nightly-2021-07-16:

Full commit log

• 0cf306e chore: fix typo

nightly-2021-07-16

Changes since nightly-2021-07-14:

Full commit log

• a8d599a fix: typo
• 7374b9b chore: update webserver demo
• eef413c chore: unused binding in FromToJson
• c7f5fd6 fix: missing interpolation in trace message
• 8d616e0 doc: fix categoryParenthesizer documentation

nightly-2021-07-14

Changes since nightly-2021-07-13:

Full commit log

• 93a3fd1 refactor: do not use explicit instance, but use deriving instead.
• 0d41fd0 feat: add xml parser.
• b5d8bc1 chore: Nix: pin LEAN_CXX for manual leanc calls

nightly-2021-07-13

Changes since nightly-2021-07-11:

Full commit log

• 2c3067e doc: bundle updated lean4.py Pygments file and lstlean.tex
• 7dc3e72 chore: update stage0
• 521ed11 chore: move parseTagged