Skip to content

Commit 2f197b3

Browse files
authored
Build on Windows (#526)
* Fix two line ending bugs to build on Windows * no backslashes * four backslashes * Enable parallel builds on Windows ("-j12" is not recognised by make.exe, we need "-j" "12")
1 parent 2c6e9ab commit 2f197b3

File tree

8 files changed

+8
-7
lines changed

8 files changed

+8
-7
lines changed

configure.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ make -f Makefile mrproper
1414

1515
if command -v coqc >/dev/null 2>&1
1616
then
17-
COQLIB=`coqc -where`
17+
COQLIB=` coqc -where | tr -d '\r' | tr '\\\\' '/'`
1818

1919
if [ "$1" == "local" ]
2020
then

coq-metacoq-checker.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
1616
license: "MIT"
1717
build: [
1818
["sh" "./configure.sh"]
19-
[make "-j%{jobs}%" "checker"]
19+
[make "-j" "%{jobs}%" "checker"]
2020
]
2121
install: [
2222
[make "-C" "checker" "install"]

coq-metacoq-erasure.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
1616
license: "MIT"
1717
build: [
1818
["sh" "./configure.sh"]
19-
[make "-j%{jobs}%" "-C" "erasure"]
19+
[make "-j" "%{jobs}%" "-C" "erasure"]
2020
]
2121
install: [
2222
[make "-C" "erasure" "install"]

coq-metacoq-pcuic.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
1616
license: "MIT"
1717
build: [
1818
["sh" "./configure.sh"]
19-
[make "-j%{jobs}%" "-C" "pcuic"]
19+
[make "-j" "%{jobs}%" "-C" "pcuic"]
2020
]
2121
install: [
2222
[make "-C" "pcuic" "install"]

coq-metacoq-safechecker.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
1616
license: "MIT"
1717
build: [
1818
["sh" "./configure.sh"]
19-
[make "-j%{jobs}%" "-C" "safechecker"]
19+
[make "-j" "%{jobs}%" "-C" "safechecker"]
2020
]
2121
install: [
2222
[make "-C" "safechecker" "install"]

coq-metacoq-template.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
1616
license: "MIT"
1717
build: [
1818
["sh" "./configure.sh"]
19-
[make "-j%{jobs}%" "template-coq"]
19+
[make "-j" "%{jobs}%" "template-coq"]
2020
]
2121
install: [
2222
[make "-C" "template-coq" "install"]

coq-metacoq-translations.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ authors: ["Simon Boulier <simon.boulier@inria.fr>"
1212
license: "MIT"
1313
build: [
1414
["sh" "./configure.sh"]
15-
[make "-j%{jobs}%" "-C" "translations"]
15+
[make "-j" "%{jobs}%" "-C" "translations"]
1616
]
1717
install: [
1818
[make "-C" "translations" "install"]

template-coq/update_plugin.sh

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ then
1414
(cd gen-src; ./to-lower.sh)
1515
rm -f gen-src/*.d
1616
# Fix an extraction bug: wrong type annotation on eq_equivalence
17+
sed -i.bak 's/\r//g' gen-src/cRelationClasses.mli
1718
patch -N -p0 < extraction.patch
1819
exit 0
1920
else

0 commit comments

Comments
 (0)