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
Dan Frumin
ReLoC-v1
Commits
0a49ea58
Commit
0a49ea58
authored
Mar 18, 2019
by
Dan Frumin
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' of gitlab.mpi-sws.org:dfrumin/logrel-conc
parents
edc1db27
12ffa3dc
Pipeline
#15591
passed with stage
in 6 minutes and 7 seconds
Changes
5
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
15 additions
and
48 deletions
+15
-48
.gitlab-ci.yml
.gitlab-ci.yml
+2
-7
Makefile
Makefile
+12
-16
README.md
README.md
+1
-1
awk.Makefile
awk.Makefile
+0
-23
ci
ci
+0
-1
No files found.
.gitlab-ci.yml
View file @
0a49ea58
image
:
ralfjung/opam-ci:
latest
image
:
ralfjung/opam-ci:
opam2
stages
:
-
build
variables
:
CPU_CORES
:
"
10"
GIT_SUBMODULE_STRATEGY
:
"
recursive"
.template
:
&template
stage
:
build
tags
:
-
fp
script
:
-
git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
-
ci/buildjob
cache
:
key
:
"
$CI_JOB_NAME"
...
...
@@ -30,8 +30,3 @@ build-coq.8.7.2:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.2
coq-mathcomp-ssreflect
version
1.6.4"
build-coq.8.6.1
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.6.1
coq-mathcomp-ssreflect
version
1.6.4"
Makefile
View file @
0a49ea58
...
...
@@ -8,15 +8,13 @@ all: Makefile.coq
clean
:
Makefile.coq
+@make
-f
Makefile.coq clean
find theories
\(
-name
"*.
v.
d"
-o
-name
"*.vo"
-o
-name
"*.aux"
-o
-name
"*.cache"
-o
-name
"*.glob"
-o
-name
"*.vio"
\)
-print
-delete
find theories
\(
-name
"*.d"
-o
-name
"*.vo"
-o
-name
"*.aux"
-o
-name
"*.cache"
-o
-name
"*.glob"
-o
-name
"*.vio"
\)
-print
-delete
rm
-f
Makefile.coq
.PHONY
:
clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
Makefile.coq
:
_CoqProject Makefile awk.Makefile
# Create Coq Makefile.
Makefile.coq
:
_CoqProject Makefile
"
$(COQBIN)
coq_makefile"
-f
_CoqProject
-o
Makefile.coq
mv
Makefile.coq Makefile.coq.tmp
&&
awk
-f
awk.Makefile Makefile.coq.tmp
>
Makefile.coq
&&
rm
Makefile.coq.tmp
# Install build-dependencies
build-dep/opam
:
opam Makefile
...
...
@@ -30,21 +28,19 @@ build-dep: build-dep/opam phony
@
# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@
# that are incompatible with our build requirements.
@
# To achieve this, we create a fake opam package that has our build-dependencies as
@
# dependencies, but does not actually install anything.
@
# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@
# package changed.
@
BUILD_DEP_PACKAGE
=
"
$$
(egrep "
^name:
" build-dep/opam | sed 's/^name: *"
\(
.
*
\)
" */
\1
/')"
;
\
echo
"# Pinning build-dep package."
&&
\
opam pin add
-k
path
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
.dev build-dep
&&
\
((!
opam
--version
|
grep
"^1
\.
"
>
/dev/null
)
||
(
\
echo
"# Reinstalling build-dep package."
&&
\
opam reinstall
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
\
))
@
# dependencies, but does not actually install anything itself.
@
echo
"# Pinning build-dep package."
&&
\
if
opam
--version
|
grep
"^1
\.
"
-q
;
then
\
BUILD_DEP_PACKAGE
=
"
$$
(egrep "
^name:
" build-dep/opam | sed 's/^name: *"
\(
.
*
\)
" */
\1
/')"
&&
\
opam pin add
-k
path
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
.dev build-dep
&&
\
opam reinstall
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
;
\
else
\
opam
install
$(OPAMFLAGS)
build-dep/
;
\
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile
:
;
_CoqProject
:
;
awk.Makefile
:
;
opam
:
;
# Phony wildcard targets
...
...
README.md
View file @
0a49ea58
...
...
@@ -12,7 +12,7 @@ The code here remains for historical reasons
This version is known to compile with:
-
Coq
8.6.1 /
8.7.2
-
Coq 8.7.2
-
Ssreflect 1.6.4
-
Autosubst branch
[
coq86-devel
](
https://github.com/uds-psl/autosubst/tree/coq86-devel
)
-
std++ version
[
32570aa6e0d04633047d9fddb3cf8da1748d9695
](
https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/32570aa6e0d04633047d9fddb3cf8da1748d9695
)
...
...
awk.Makefile
deleted
100644 → 0
View file @
edc1db27
# awk program that patches the Makefile generated by Coq.
# Detect the name this project will be installed under.
/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
# we can just split the string at '/' here.
split($0, PIECES, /\//);
PROJECT=PIECES[2];
}
# Patch the uninstall target to work properly, and to also uninstall stale files.
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
# This (and the section above) can be removed once we no longer support Coq 8.6.
/^uninstall: / {
print "uninstall:";
print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
getline;
next
}
# This forwards all unchanged lines
1
ci
@
99c935d2
Compare
99c935d2
...
99c935d2
Subproject commit 99c935d2007358fe4028560e96f9c136e608e696
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