Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Sophie Quinton
rt-proofs
Commits
ac5ccfe0
Commit
ac5ccfe0
authored
Jul 14, 2016
by
Felipe Cerqueira
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix create_makefile script to work on Mac and Linux
parent
170ca73b
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
24 additions
and
4 deletions
+24
-4
create_makefile.sh
create_makefile.sh
+24
-4
No files found.
create_makefile.sh
View file @
ac5ccfe0
# Compile all *.v files (except the ones that define the decidable equality). Those
# Compile all *.v files (except the ones that define the decidable equality). Those
# are directly included in other files.
# are directly included in other files.
coq_makefile
-f
_CoqProject
$(
find
-name
"*.v"
!
-name
"*#*"
!
-name
"*eqdec*.v"
-print
)
-o
Makefile
coq_makefile
-f
_CoqProject
$(
find
.
-name
"*.v"
!
-name
"*#*"
!
-name
"*eqdec*.v"
-print
)
-o
Makefile
# Fix the 'make validate' command. It doesn't handle the library prefix properly
# Fix the 'make validate' command. It doesn't handle the library prefix properly
# and cause clashes for files with the same name. This forces full filenames and
# and cause clashes for files with the same name. This forces full filenames and
# adds the rt. prefix
# adds the rt. prefix
sed
-i
's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g'
Makefile
if
[
"
$(
uname
)
"
==
"Darwin"
]
;
then
sed
-i
''
's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g'
Makefile
elif
[
"
$(
expr
substr
$(
uname
-s
)
1 5
)
"
==
"Linux"
]
;
then
sed
-i
's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g'
Makefile
elif
[
"
$(
expr
substr
$(
uname
-s
)
1 10
)
"
==
"MINGW32_NT"
]
;
then
:
fi
# Fix 'make html' so that it parses comments and has links to ssreflect.
# Fix 'make html' so that it parses comments and has links to ssreflect.
sed
-i
's|-interpolate -utf8|-interpolate -utf8 --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g'
Makefile
if
[
"
$(
uname
)
"
==
"Darwin"
]
;
then
sed
-i
''
's|-interpolate -utf8|-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g'
Makefile
elif
[
"
$(
expr
substr
$(
uname
-s
)
1 5
)
"
==
"Linux"
]
;
then
sed
-i
's|-interpolate -utf8|-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g'
Makefile
elif
[
"
$(
expr
substr
$(
uname
-s
)
1 10
)
"
==
"MINGW32_NT"
]
;
then
:
fi
# Fix 'make clean' to remove all binary files, regardless of name
# Fix 'make clean' to remove all binary files, regardless of name
sed
-i
's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g'
Makefile
if
[
"
$(
uname
)
"
==
"Darwin"
]
;
then
sed
-i
''
's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g'
Makefile
elif
[
"
$(
expr
substr
$(
uname
-s
)
1 5
)
"
==
"Linux"
]
;
then
sed
-i
's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g'
Makefile
elif
[
"
$(
expr
substr
$(
uname
-s
)
1 10
)
"
==
"MINGW32_NT"
]
;
then
:
fi
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment