nightly-2021-08-16

Changes since nightly-2021-08-15:

Full commit log

• 4fe65f3 test: mathport issue https://github.com/dselsam/mathport/issues/18
• 9182ebd feat: elaborate * simp argument
• 3c68703 feat: elaborate <- modifier at simp arguments
• d4410c2 chore: update stage0
• 7c5ab8b chore: prepare to add <- as simp argument
• 2534445 feat: add simpStar parser
• cbd36e8 chore: remove ToExpr Expr

nightly-2021-08-15

Changes since nightly-2021-08-13:

Full commit log

• d8340f5 doc: document new binop% elaborator
• d52de33 chore: remove workaround
• fc6f932 chore: update stage0
• a15a36b chore: cleanup Subarray instances
• ddec62f feat: synthesize pending metavariables created before binop% too
• 2994747 chore: remove workaround
• 7de3846 chore: update stage0
• 4ee2f80 fix: improve binop% elaborator
• 4239ae6 chore: fix tests
• 4b58c4c refactor: instances that "hide" coercions
• 452b717 chore: update stage0
• ef46b01 chore: use binop% to define the notations >> and <|>
• b012050 chore: remove some macros that use binop%
• 3418eb7 fix: check whether CoeHTCT has already been defined or not at hasCoe
• be23709 chore: use binop% to define ++ notation
• d3d03df feat: new elaborator for binop%

nightly-2021-08-13

Changes since nightly-2021-08-12:

Full commit log

• 24fe287 chore: change Pow class
• d3f007b chore: fix stdlib benchmarks
• 16026e9 perf: restore monad instance specialization hack
• a6b6d61 chore: simplify mkProjStx?
• da03262 fix: check redundant sources at structure instance notation
• 917eb4d chore: collect stdlib compilation flags in new header
• 7e78de9 doc: further bootstrapping complications
• 9c15f94 perf: do not use parsers from the current stage inside quotations by default
• 20accf5 feat: revise macro parameter syntax
• 6c22042 chore: adjust stx precedences
• bf313a9 chore: update stage0
• 28fe8e7 chore: update stage0
• c68882c feat: structure instance notation with multiple sources
• a02a490 feat: add mkProjStx?
• 2dfde46 fix: index out of bounds
• accf198 feat: add ExplicitSourceInfo
• c591902 refactor: add structure to Source.explicit
• 45e4dc2 refactor: simplify Source.explicit
• 5952a85 feat: pp.analyze improve heuristics for fun binders
• 638d0ca feat: pp.instances and pp.instanceTypes
• 040141f feat: unexpander for Subtype
• 67103f5 chore: add TODOs for multiple sources
• 74bd537 fix: generation of to* field names
• d78101f chore: remove mutual recursion workaround
• 4abbb3d chore: cleanup
• f1738ce feat: add macro for expanding field abbrev notation
• 00ec22d chore: update stage0
• 09c2b66 feat: allow multiple sources in the structure instance parser

nightly-2021-08-12

Changes since nightly-2021-08-11:

Full commit log

• efb3f52 fix: handle MData-wrapped app fns consistently in delaborator
• 6352e54 test: add classes up to Field
• 3b43ab4 fix: formatter: check for comment tokens
• c591a68 chore: Nix: add back overrideCC that got lost on the way
• d471f8d fix: fixes #621
• 39ce304 feat: emit warning message when failed to copy default value
• 61b3e6b fix: reduce projections of expanded structures at copyDefaultValue?
• 63ad42b refactor: move and generalize reduceProj?
• 0623bb3 feat: update fieldMap with composite field
• ae03f15 test: default value set at copied structure
• 3b1285b feat: process overriden default values in copied parents
• 295cae8 feat: copy field default values
• 47b8fa1 fix: propagate visibility annotation

nightly-2021-08-11

Changes since nightly-2021-08-10:

Full commit log

• 702a249 chore: update stage0
• 16ea005 fix: fixes #620
• 972f00b fix: pending metavariable issue
• 7cec205 feat: add instance Alternative (MonadCacheT α β m)
• f4433f3 feat: add Alternative (StateRefT' ω σ m)
• b226ae7 test: add CommGroup diamond
• 9cd7292 fix: missing instantiateMVars
• 9fe1cd1 chore: modify default value for option structureDiamondWarning
• d03fa17 test: copyNewFieldsFrom
• 50deae9 feat: copy binderInfo and inferMod from original field
• bc26a9b feat: improve copyNewFieldsFrom
• af1cecc feat: better error message
• 9e5998b feat: register instance/reducible attribute for structuer diamond coercions
• 0f184a8 fix: binder annotation for class diamond coercions
• 2b71e16 test: structure diamond coercion
• 0b3e548 fix: syntax tree returned by syntax elaborator
• 4089fca chore: update stage0
• bccad8e feat: add coercion to parent structure whose fields having been copied
• 97664de fix: diamonds with dependent fields
• e8403f8 fix: ensure field names are atomic
• 5271068 chore: update stage0
• 6f318dd feat: save binderInfo and inferMod ad registerStructure
• 80cf520 chore: update stage0
• 5ef7205 feat: save additional information at StructureFieldInfo
• f67501a chore: cleanup
• a0bd964 test: overriding default value of private field
• 3f3e5d9 fix: private field + default value bug
• 3896c44 chore: fix incorrect comment
• fdce7a9 feat: structure diamonds basic support
• 56c2f59 feat: add getFieldType

nightly-2021-08-10

Changes since nightly-2021-08-09:

Full commit log

• 0118c47 refactor: separate pp.funBinderTypes and pp.piBinderTypes
• 4e7cb76 chore: Nix: adjust local cache config

nightly-2021-08-09

Changes since nightly-2021-08-08:

Full commit log

• 119f685 doc: fix link
• 40274e4 chore: fix docs
• 341b4ac doc: link to some macro documentation

nightly-2021-08-08

Changes since nightly-2021-08-07:

Full commit log

• 358a129 fix: protect rfl
• ba6fcd7 chore: update stage0
• 1d9d8c7 chore: fix tests
• 9cc9429 chore: remove staging workaround theorems
• f1272f7 chore: update stage0
• a821dcb chore: enforce naming convention for theorems
• a0c2142 chore: update stage0
• a863f1b fix: fixes #616
• 8a84532 feat: add PEmpty
• 6e2b718 fix: fixes #242
• d482212 feat: add Meta.abstract

nightly-2021-08-07

Changes since nightly-2021-08-06:

Full commit log

• 9dc2a42 test: add test for getModuleDoc?
• f2bbe22 chore: update stage0
• 8acbb55 chore: fix tests
• 3293e9e chore: fix module comments, they must occur after the imports
• accdede test: module docs
• 5796b93 fix: support for /-! at whitespace
• dca9278 feat: add elabModuleDoc
• 1fc1c4f chore: update stage0
• 3d485bf feat: add moduleDocExt
• 8d5964c feat: add module doc parser
• 634f501 chore: update stage0
• 7587218 chore: fix test
• 1be41f2 chore: fix stdlib
• 8184667 chore: update stage0
• 76cc991 fix: fixes #370
• a230fe2 fix: forallMetaTelescope issue
• 803b73e chore: update stage0
• 01985f4 fix: actually interpret imported anonymous [init] decls
• c6e1e35 perf: trace messages should disable pp.analyze
• 090786f chore: Nix: fix doc sources
• 34a27f2 fix: pp.analyze strict implicits
• bae3185 chore: Nix: do not install Cachix if not authenticated
• 557af62 chore: Nix: do not include temci by default
• 2cf780f chore: Nix: cache store
• e79d52d chore: Nix: reduce doc/doc-test sources
• 14177fb feat: misc pp.analyze improvements
• 8140010 chore: Nix: go back to LLVM 11 on macOS
• 84b155c chore: add docstring
• 56320cb chore: naming convention and cleanup
• bcfc927 fix: fixes #602
• 789c707 fix: avoid eager TC synthesis at isDefEq

nightly-2021-08-06

Changes since nightly-2021-08-05:

Full commit log

• ddbd10f chore: update stage0
• 5f019a9 chore: update stage0
• 4dbb3e6 fix: add workaround to prevent code explosion at deriving for FromJson
• d52908d chore: LLVM: 10 -> 12
• c78bbc6 chore: Nix: update inputs
• 9ef2345 perf: enforce hash map load factor
• 1b44768 chore: fix test
• 3bbf19a feat: FromToJson for nested inductives
• 07d1735 feat: borrow inference: preserve mutual tail calls
• 4cdfbde fix: pp.analyze also bottom-up the trivials
• 1a815a4 perf: pp.analyze add quick check
• b86e9a3 fix: pp.analyze bottom-up only checks unknown types
• 7807f09 chore: update stage0
• 1f0e0a7 doc: document alternative design option
• 72e7bf4 fix: synthPending bug
• aff28f5 fix: fixes #604
• 0869bbe fix: missig registerMVarErrorImplicitArgInfo for postponed instance mvars
• 91b60cb chore: indentation
• 61cdf93 fix: missing registerMVarErrorImplicitArgInfo