From bb6628a4c45f93d4d89dc1a686ad413754436b5e Mon Sep 17 00:00:00 2001 From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com> Date: Sun, 21 Nov 2021 13:55:15 +0100 Subject: [PATCH 1/7] Get `make` to work on Windows --- CONTRIBUTING.md | 2 ++ GNUmakefile | 2 +- INSTALL.md | 14 +++++++++++--- MAKEWINDOWS.md | 27 +++++++++++++++++++++++++++ 4 files changed, 41 insertions(+), 4 deletions(-) create mode 100644 MAKEWINDOWS.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e0a5a12029..b9450a2ae6 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -8,6 +8,8 @@ When preparing a PR here are some general guidelines: which will generate all required `Everything` files in `Cubical/README.agda` and then typecheck the latter file. + - If you're using Windows, [here](MAKEWINDOWS.md) are some instructions to get the `make` command working. + - Please read through and clean your code before making a PR. Clean code has reasonable line length (<100 characters), good indentation, appropriate amounts of comments and consistent naming. diff --git a/GNUmakefile b/GNUmakefile index 3de8a05bf9..8870856137 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_EXEC?=agda -W error -W noNoEquivWhenSplitting FIX_WHITESPACE?=fix-whitespace RTS_OPTIONS=+RTS -H3G -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) -RUNHASKELL?=runhaskell +RUNHASKELL?=runghc EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs .PHONY : all diff --git a/INSTALL.md b/INSTALL.md index bfcdb881ec..aa4e9c07e7 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -86,7 +86,9 @@ Once this works go to a suitable directory and run > make ``` -This should compile all of the agda/cubical files. To test that it +This should compile all of the agda/cubical files. (If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). + +To test that it works in emacs run ``` @@ -119,6 +121,8 @@ in a cabal sandbox do the following: > make ``` +(If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). + If you have cabal v2 installed the sandbox command should be replaced by `cabal v1-sandbox init`. @@ -167,7 +171,9 @@ Once this works go to a suitable directory and run > make ``` -This should compile all of the agda/cubical files. To test that it +This should compile all of the agda/cubical files. (If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). + +To test that it works in emacs run ``` @@ -251,7 +257,9 @@ Once this works go to a suitable directory and run > make ``` -This should compile all of the agda/cubical files. To test that it +This should compile all of the agda/cubical files. (If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). + +To test that it works in emacs run ``` diff --git a/MAKEWINDOWS.md b/MAKEWINDOWS.md new file mode 100644 index 0000000000..1046ca579d --- /dev/null +++ b/MAKEWINDOWS.md @@ -0,0 +1,27 @@ +# Instructions for getting `make` to work on Windows + +The GNU command `make` does not work on Windows out of the box. Here are the steps I took to get it to work on my Windows 10 machine: + +1. You probably already installed the Chocolatey package manager when installing Agda (check by running `choco` in terminal). If not, install it from [here](https://chocolatey.org/install). + +2. You need to install the `make` command by running + ``` + choco install make + ``` + +3. The makefile runs the `runhaskell` command, which might not work on your system. Test this by running in terminal + ``` + runhaskell + ``` + If that doesn't work, you'll have to change line 5 of `~/GNUmakefile` to + ``` + RUNHASKELL?=runghc + ``` + +4. Give your user account `Read & Execute` access to `C:\Windows\System32\pthread.dll` + +5. In terminal, run + ``` + chcp.com 65001 + ``` + so that Haskell can parse UTF-8 characters. \ No newline at end of file From 4a02a85a4a179a1c5de3ed7a9f4388ac5d903b37 Mon Sep 17 00:00:00 2001 From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com> Date: Mon, 22 Nov 2021 13:41:17 +0100 Subject: [PATCH 2/7] fixes --- GNUmakefile | 2 +- MAKEWINDOWS.md | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/GNUmakefile b/GNUmakefile index 8870856137..3de8a05bf9 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_EXEC?=agda -W error -W noNoEquivWhenSplitting FIX_WHITESPACE?=fix-whitespace RTS_OPTIONS=+RTS -H3G -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) -RUNHASKELL?=runghc +RUNHASKELL?=runhaskell EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs .PHONY : all diff --git a/MAKEWINDOWS.md b/MAKEWINDOWS.md index 1046ca579d..3244fd322c 100644 --- a/MAKEWINDOWS.md +++ b/MAKEWINDOWS.md @@ -9,18 +9,19 @@ The GNU command `make` does not work on Windows out of the box. Here are the ste choco install make ``` -3. The makefile runs the `runhaskell` command, which might not work on your system. Test this by running in terminal +3. The [makefile](GNUmakefile) runs the `runhaskell` command, which might not work on your system. Test this by running in terminal ``` runhaskell ``` - If that doesn't work, you'll have to change line 5 of `~/GNUmakefile` to + If that doesn't work, create a file called `runhaskell.bat` with the contents ``` - RUNHASKELL?=runghc + runghc %* ``` + and put this somewhere in your PATH. 4. Give your user account `Read & Execute` access to `C:\Windows\System32\pthread.dll` -5. In terminal, run +5. Now, each time before you run `make`, run the following command in your terminal: ``` chcp.com 65001 ``` From 2d1b0345c836dc83347be4b0e75324c0269fc2c2 Mon Sep 17 00:00:00 2001 From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com> Date: Fri, 26 Nov 2021 10:33:56 +0100 Subject: [PATCH 3/7] Emphasise --- MAKEWINDOWS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MAKEWINDOWS.md b/MAKEWINDOWS.md index 3244fd322c..65b12f7cfc 100644 --- a/MAKEWINDOWS.md +++ b/MAKEWINDOWS.md @@ -21,7 +21,7 @@ The GNU command `make` does not work on Windows out of the box. Here are the ste 4. Give your user account `Read & Execute` access to `C:\Windows\System32\pthread.dll` -5. Now, each time before you run `make`, run the following command in your terminal: +5. Now, **each time before you run `make`,** run the following command in your terminal: ``` chcp.com 65001 ``` From 95225e6ee16dfbf6e7f7648eb4f97ec452bed653 Mon Sep 17 00:00:00 2001 From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com> Date: Fri, 26 Nov 2021 11:45:11 +0100 Subject: [PATCH 4/7] Fix whitespace --- MAKEWINDOWS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MAKEWINDOWS.md b/MAKEWINDOWS.md index 65b12f7cfc..2ed91d6254 100644 --- a/MAKEWINDOWS.md +++ b/MAKEWINDOWS.md @@ -25,4 +25,4 @@ The GNU command `make` does not work on Windows out of the box. Here are the ste ``` chcp.com 65001 ``` - so that Haskell can parse UTF-8 characters. \ No newline at end of file + so that Haskell can parse UTF-8 characters. From 1d5a6610926d84bb32aef23ffc1978bd8b1b7071 Mon Sep 17 00:00:00 2001 From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com> Date: Wed, 15 Dec 2021 16:27:51 +0100 Subject: [PATCH 5/7] line length --- CONTRIBUTING.md | 4 ++-- MAKEWINDOWS.md | 10 +++++++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b9450a2ae6..e92036b479 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -7,8 +7,8 @@ When preparing a PR here are some general guidelines: - To test your changes before submission, run `make` at the top level, which will generate all required `Everything` files in `Cubical/README.agda` and then typecheck the latter file. - - - If you're using Windows, [here](MAKEWINDOWS.md) are some instructions to get the `make` command working. + If you're using Windows, [here](MAKEWINDOWS.md) are some instructions + to get the `make` command working. - Please read through and clean your code before making a PR. Clean code has reasonable line length (<100 characters), good indentation, diff --git a/MAKEWINDOWS.md b/MAKEWINDOWS.md index 2ed91d6254..296ef7fdc1 100644 --- a/MAKEWINDOWS.md +++ b/MAKEWINDOWS.md @@ -1,15 +1,19 @@ # Instructions for getting `make` to work on Windows -The GNU command `make` does not work on Windows out of the box. Here are the steps I took to get it to work on my Windows 10 machine: +The GNU command `make` does not work out of the box on Windows. +Here are some steps you could take to get `make` working on a Windows machine: -1. You probably already installed the Chocolatey package manager when installing Agda (check by running `choco` in terminal). If not, install it from [here](https://chocolatey.org/install). +1. You probably already installed the Chocolatey package manager when + installing Agda (check by running `choco` in terminal). If not, install it + from [here](https://chocolatey.org/install). 2. You need to install the `make` command by running ``` choco install make ``` -3. The [makefile](GNUmakefile) runs the `runhaskell` command, which might not work on your system. Test this by running in terminal +3. The [makefile](GNUmakefile) runs the `runhaskell` command, which might not + work on your system. Test this by running in terminal ``` runhaskell ``` From 6ef0db3a245a083f852e6a1eec4449dc24bd49f3 Mon Sep 17 00:00:00 2001 From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com> Date: Wed, 15 Dec 2021 16:28:56 +0100 Subject: [PATCH 6/7] Revert INSTALL.md --- INSTALL.md | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index aa4e9c07e7..7a30e879f8 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -86,9 +86,7 @@ Once this works go to a suitable directory and run > make ``` -This should compile all of the agda/cubical files. (If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). - -To test that it +This should compile all of the agda/cubical files. To test that it works in emacs run ``` @@ -121,8 +119,6 @@ in a cabal sandbox do the following: > make ``` -(If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). - If you have cabal v2 installed the sandbox command should be replaced by `cabal v1-sandbox init`. @@ -171,9 +167,7 @@ Once this works go to a suitable directory and run > make ``` -This should compile all of the agda/cubical files. (If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). - -To test that it +This should compile all of the agda/cubical files. To test that it works in emacs run ``` @@ -257,9 +251,7 @@ Once this works go to a suitable directory and run > make ``` -This should compile all of the agda/cubical files. (If you're on Windows, see [here](MAKEWINDOWS.md) for instructions on using `make`). - -To test that it +This should compile all of the agda/cubical files. To test that it works in emacs run ``` @@ -286,4 +278,4 @@ $ cat .agda/defaults cubical $ cat .agda/libraries /path/to/cubical.agda-lib -``` +``` \ No newline at end of file From f0757060d9d2d4b265fd8169635eae7c3ed32175 Mon Sep 17 00:00:00 2001 From: Jordan Barrett <90195985+barrettj12@users.noreply.github.com> Date: Wed, 15 Dec 2021 16:34:29 +0100 Subject: [PATCH 7/7] fix whitespace --- INSTALL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/INSTALL.md b/INSTALL.md index 7a30e879f8..bfcdb881ec 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -278,4 +278,4 @@ $ cat .agda/defaults cubical $ cat .agda/libraries /path/to/cubical.agda-lib -``` \ No newline at end of file +```