From 170fac871caa3459116845707ba4c0413167b5f3 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 1 Jun 2024 23:19:20 -0400 Subject: [PATCH] build: generate gitignore --- .gitignore | 4 ---- aya/guide/prover-tutorial.aya.md | 2 +- scripts/build-aya.js | 6 ++++++ src/.gitignore | 2 ++ 4 files changed, 9 insertions(+), 5 deletions(-) create mode 100644 src/.gitignore diff --git a/.gitignore b/.gitignore index 8c2f417..65815e1 100644 --- a/.gitignore +++ b/.gitignore @@ -8,7 +8,3 @@ yarn-error.log* pnpm-debug.log* dist build-aya/ - -src/guide/haskeller-tutorial.md -src/guide/anqur-story.md -src/guide/ext-types.md diff --git a/aya/guide/prover-tutorial.aya.md b/aya/guide/prover-tutorial.aya.md index 83f5a68..2d33672 100644 --- a/aya/guide/prover-tutorial.aya.md +++ b/aya/guide/prover-tutorial.aya.md @@ -91,7 +91,7 @@ This will need some advanced proving techniques that are beyond the scope of thi simple tutorial, so I'll skim them. First, we need type-safe coercion: ```aya -def cast (p : A ↑ = B) : A -> B => coe 0 1 (fn i => p i) +def cast (p : A ↑ = B) : A -> B => ↑ coe 0 1 (fn i => p i) ``` Then, from `q : b = c` we construct the equivalence `(a = b) = (a = c)` diff --git a/scripts/build-aya.js b/scripts/build-aya.js index 839cca2..2abb4e9 100644 --- a/scripts/build-aya.js +++ b/scripts/build-aya.js @@ -43,6 +43,7 @@ walk(".", (file) => { }); // Put preprocessed files to src/ process.chdir("../build-aya"); +let gitignore = ""; walk(".", (file) => { console.log("Moving: " + file); const dest = path.resolve("../src", file); @@ -52,4 +53,9 @@ walk(".", (file) => { if (err) throw err; }); }); + gitignore += file + "\n"; +}); + +fs.writeFile("../src/.gitignore", gitignore, (err) => { + if (err) throw err; }); diff --git a/src/.gitignore b/src/.gitignore new file mode 100644 index 0000000..21e7913 --- /dev/null +++ b/src/.gitignore @@ -0,0 +1,2 @@ +guide/haskeller-tutorial.md +guide/prover-tutorial.md