diff --git a/Makefile b/Makefile index a4a7eb4..d2a84a9 100644 --- a/Makefile +++ b/Makefile @@ -4,14 +4,7 @@ LIB_DIR = ./lib TEST_PASS_DIR = ./test/should-pass TEST_ERROR_DIR = ./test/should-error -default: tests tests-lib # check_docs - -# Problem regarding the docs: github pages markdown is not compatible -# with using entangled, so the entangled syntax is currently commented -# out. We need a way to automatically put the entangled syntax back in -# and then run deduce on these files. -Jeremy - -check_docs: check_index check_fun check_intro check_ref +default: tests tests-lib tests-should-pass: $(PYTHON) ./deduce.py --recursive-descent $(TEST_PASS_DIR) --dir $(LIB_DIR) @@ -21,36 +14,9 @@ tests-should-error: $(PYTHON) ./deduce.py --recursive-descent $(TEST_ERROR_DIR) --error --dir $(LIB_DIR) $(PYTHON) ./deduce.py --lalr $(TEST_ERROR_DIR) --error --dir $(LIB_DIR) - tests-lib: $(PYTHON) ./deduce.py ./lib --recursive-descent --dir $(LIB_DIR) -# List parsing needs to be updated in Deduce.lark -# $(PYTHON) ./deduce.py . --lalr + $(PYTHON) ./deduce.py ./lib --lalr --dir $(LIB_DIR) tests: tests-should-pass tests-should-error -check_index: - /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent index.pf --dir $(LIB_DIR) - $(PYTHON) ./deduce.py --lalr index.pf --dir $(LIB_DIR) - -check_fun: - /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent FunctionalProgramming.pf --dir $(LIB_DIR) -# List parsing needs to be updated in Deduce.lark -# $(PYTHON) ./deduce.py --lalr FunctionalProgramming.pf - -check_intro: - /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent ProofIntro.pf --dir $(LIB_DIR) -# List parsing needs to be updated in Deduce.lark -# $(PYTHON) ./deduce.py --lalr ProofIntro.pf --dir $(LIB_DIR) - -check_ref: - /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent Reference.pf --dir $(LIB_DIR) - $(PYTHON) ./deduce.py --lalr Reference.pf --dir $(LIB_DIR) - -clean: - rm -f index.pf FunctionalProgramming.pf ProofIntro.pf - rm -rf .entangled diff --git a/README.md b/README.md index d15c613..0b1c59f 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,9 @@ -See the web page for Deduce: +The web page for Deduce is at the following link: [https://jsiek.github.io/deduce/](https://jsiek.github.io/deduce/) + +The directory structure: +* `/doc` Documentation for Deduce +* `/test` Deduce files used for testing Deduce. +* diff --git a/FunctionalProgramming.md b/doc/FunctionalProgramming.md similarity index 100% rename from FunctionalProgramming.md rename to doc/FunctionalProgramming.md diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 0000000..e751ae6 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,36 @@ +PYTHON = $(shell command -v python3.11) + +LIB_DIR = ../lib + +default: check_docs + +# Problem regarding the docs: github pages markdown is not compatible +# with using entangled, so the entangled syntax is currently commented +# out. We need a way to automatically put the entangled syntax back in +# and then run deduce on these files. -Jeremy + +check_docs: check_index check_fun check_intro check_ref + +check_index: + /Users/jsiek/Library/Python/3.11/bin/entangled tangle + $(PYTHON) ./deduce.py --recursive-descent index.pf --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr index.pf --dir $(LIB_DIR) + +check_fun: + /Users/jsiek/Library/Python/3.11/bin/entangled tangle + $(PYTHON) ./deduce.py --recursive-descent FunctionalProgramming.pf --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr FunctionalProgramming.pf + +check_intro: + /Users/jsiek/Library/Python/3.11/bin/entangled tangle + $(PYTHON) ./deduce.py --recursive-descent ProofIntro.pf --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr ProofIntro.pf --dir $(LIB_DIR) + +check_ref: + /Users/jsiek/Library/Python/3.11/bin/entangled tangle + $(PYTHON) ./deduce.py --recursive-descent Reference.pf --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr Reference.pf --dir $(LIB_DIR) + +clean: + rm -f index.pf FunctionalProgramming.pf ProofIntro.pf + rm -rf .entangled diff --git a/ProofIntro.md b/doc/ProofIntro.md similarity index 100% rename from ProofIntro.md rename to doc/ProofIntro.md diff --git a/Reference.md b/doc/Reference.md similarity index 100% rename from Reference.md rename to doc/Reference.md diff --git a/index.md b/index.md index 441c9d2..6c16748 100644 --- a/index.md +++ b/index.md @@ -101,8 +101,8 @@ This introduction to Deduce has two parts. The first part gives a tutorial on how to write functional programs in Deduce. The second part shows how to write proofs in Deduce. -* [Functional Programming in Deduce](./FunctionalProgramming.md) -* [Writing Proofs in Deduce](./ProofIntro.md) +* [Functional Programming in Deduce](./doc/FunctionalProgramming.md) +* [Writing Proofs in Deduce](./doc/ProofIntro.md) I recommend that you work through the examples in this introduction. Create a file named `examples.pf` in the top `deduce` @@ -121,7 +121,7 @@ You can also download one of these extensions for programming in Deduce in some The Deduce Reference manual is linked to below. It provides an alphabetical list of all the features in Deduce. -* [Reference Manual](./Reference.md) +* [Reference Manual](./doc/Reference.md) ## Syntax/Grammar Overview