Skip to content

Commit

Permalink
chore: update stage0 (#3041)
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Dec 8, 2023
1 parent c474dff commit 00359a0
Show file tree
Hide file tree
Showing 31 changed files with 27,371 additions and 17,094 deletions.
9 changes: 5 additions & 4 deletions stage0/src/CMakeLists.txt

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions stage0/src/lean-toolchain

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions stage0/src/runtime/io.cpp

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion stage0/src/runtime/mpz.cpp

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion stage0/src/stdlib.make.in

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion stage0/src/stdlib_flags.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ options get_default_options() {
// switch to `true` for ABI-breaking changes affecting meta code
opts = opts.update({"interpreter", "prefer_native"}, false);
// switch to `true` for changing built-in parsers used in quotations
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
// toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
// with custom precheck hooks were affected
opts = opts.update({"quotPrecheck"}, true);
Expand Down
1,117 changes: 593 additions & 524 deletions stage0/stdlib/Init/Meta.c

Large diffs are not rendered by default.

14 changes: 7 additions & 7 deletions stage0/stdlib/Lean/Compiler/LCNF/AuxDeclCache.c

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading

0 comments on commit 00359a0

Please sign in to comment.