Skip to content

Commit

Permalink
chore: update stage0
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Jan 9, 2024
1 parent 06e5276 commit 1307173
Show file tree
Hide file tree
Showing 75 changed files with 119,009 additions and 118,628 deletions.
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
330 changes: 330 additions & 0 deletions stage0/stdlib/Init/Data/Range.c

Large diffs are not rendered by default.

136 changes: 68 additions & 68 deletions stage0/stdlib/Lean/Attributes.c

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions stage0/stdlib/Lean/Compiler/CSimpAttr.c

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

164 changes: 82 additions & 82 deletions stage0/stdlib/Lean/Compiler/ExternAttr.c

Large diffs are not rendered by default.

Loading

0 comments on commit 1307173

Please sign in to comment.