max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Data
History
Mac Malone d95e741824
feat: lean CLI option to print messages as JSON (#3939) 
Adds a `--json` option to the `lean` CLI. When used, the Lean frontend
will print messages as JSON objects using the default `ToJson` encoding
for the `Message` structure. This allows consumers (such as Lake) to
handle Lean output in a more intelligent, well-structured way.

`Message` has been refactored into `BaseMessage`, `Message`, and
`SerialMessage` to enable deriving `ToJson`/ `FromJson` instances
automatically for `BaseMessage` / `SerialMessage`. `SerialMessage` is a
`Message` with its `MessageData` eagerly serialized to a `String`.
2024-04-22 15:45:32 +00:00
..
Json feat: UTF-8 string validation (#3958) 2024-04-20 18:36:37 +00:00
Lsp fix: semantic tokens performance (#3932) 2024-04-18 07:48:44 +00:00
Xml chore: reorganising to reduce imports (#3790) 2024-03-27 11:15:01 +00:00
Array.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
AssocList.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Format.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
FuzzyMatching.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
HashMap.lean perf: fix linearity in (HashSet|HashMap).erase (#3887) 2024-04-12 08:54:21 +00:00
HashSet.lean perf: fix linearity in (HashSet|HashMap).erase (#3887) 2024-04-12 08:54:21 +00:00
Json.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
JsonRpc.lean feat: snapshot trees and language processors (#3014) 2024-03-14 13:40:08 +00:00
KVMap.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LBool.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LOption.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Lsp.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Name.lean chore: remove the coercion from String to Name (#3589) 2024-03-21 23:46:03 +00:00
NameMap.lean chore: remove the coercion from String to Name (#3589) 2024-03-21 23:46:03 +00:00
NameTrie.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
OpenDecl.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Options.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Parsec.lean perf: ensure linearity in Parsec.many*Core (#3830) 2024-04-22 03:41:06 +00:00
PersistentArray.lean chore: extend GetElem with getElem! and getElem? (#3694) 2024-03-28 01:42:00 +00:00
PersistentHashMap.lean fix: simp usedSimps (#3821) 2024-04-02 00:50:06 +00:00
PersistentHashSet.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Position.lean feat: lean CLI option to print messages as JSON (#3939) 2024-04-22 15:45:32 +00:00
PrefixTree.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Rat.lean chore: reorganising to reduce imports (#3790) 2024-03-27 11:15:01 +00:00
RBMap.lean chore: upstream solve_by_elim (#3408) 2024-02-21 01:16:04 +00:00
RBTree.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SMap.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SSet.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Trie.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Xml.lean chore: add missing copyright headers (#3411) 2024-02-20 01:49:55 +00:00