Skip to content

Conversation

@robsimmons
Copy link
Member

@robsimmons robsimmons commented Apr 15, 2024

This was a feature I strongly resisted adding in the Mediawiki days, but I think the greatly simplified TwelfTag system we've got going makes it quite a bit more doable.

Also adds type-safety-for-the-stlc as a test of the feature. That file has the header

%%! title: "Type safety for the simply-typed lambda calculus"
%%! import: simply-typed-lambda-calculus.elf

which causes all the Twelf code to be checked as if the contents of simply-typed-lambda-calculus.elf was included before the file. This has #import semantics from Objective-C, or #include C preprocessor semantics where IFDEF is used correctly: multiple dependencies are allowed all transitive dependencies are included, but only once. This would allow there to be one file that contains natural numbers with no imports, a second file that decribes less-than

%%! title: "Inequality for nats"
%%! import: nat.elf

and a third file that describes addition

%%! title: "Addition for nats"
%%! import: nat.elf

then, a fourth file could have the following imports

%%! title: "Addition for nats"
%%! import: nat.elf
%%! import: inequality-nat.elf
%%! import: addition-nat.elf

and

  • the nat.elf import is optional, because it will be included as a transitive dependency
  • both the inequality-nat.elf and addition.nat definitions will use the same defnition of nat which is only defined once, in nat.elf.

Comment on lines +32 to +42
exec("node elf-watcher.mjs", { cwd: "../wiki/" });
const WIKI_TWELF_LOC = "../wiki/pages/";
const cfgs = [];
for (const file of readdirSync(WIKI_TWELF_LOC)) {
if (file.endsWith(".elf")) {
if (file.endsWith(".cfg")) {
const base = file.slice(0, file.length - 4);
if (IGNORED_WIKI_FILES.has(base)) continue;
const cfg = base + ".cfg";
writeFileSync(WIKI_TWELF_LOC + cfg, file);
cfgs.push(
`test${
UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : ""
} ${WIKI_TWELF_LOC}${cfg}`
} ${WIKI_TWELF_LOC}${file}`
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Moving the cfg auto-generation into the wiki project means we can just invoke that auto-generation to run the regression tests.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants