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
Iris
stdpp
Commits
aad23129
Commit
aad23129
authored
Feb 07, 2017
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'ralf/buildsys' into 'master'
update build system and README See merge request !1
parents
10c2f692
2d8a4eb4
Pipeline
#3837
passed with stage
in 9 minutes and 26 seconds
Changes
5
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
32 additions
and
10 deletions
+32
-10
.gitlab-ci.yml
.gitlab-ci.yml
+18
-1
Makefile
Makefile
+3
-3
README.md
README.md
+3
-3
build/opam-pins.sh
build/opam-pins.sh
+7
-2
opam
opam
+1
-1
No files found.
.gitlab-ci.yml
View file @
aad23129
image
:
ralfjung/opam-ci:latest
stdpp-coq8.5
:
tags
:
-
coq
script
:
# prepare
-
. build/opam-ci.sh coq 8.5.3
# build
-
'
time
make
-j8'
cache
:
key
:
"
coq8.5"
paths
:
-
opamroot/
only
:
-
master
-
ci
-
timing
stdpp-coq8.6
:
tags
:
-
coq
...
...
@@ -10,7 +27,7 @@ stdpp-coq8.6:
-
'
time
make
-j8
TIMED=y
2>&1
|
tee
build-log.txt'
-
'
if
fgrep
Axiom
build-log.txt
>/dev/null;
then
exit
1;
fi'
-
'
cat
build-log.txt
|
egrep
"[a-zA-Z0-9_/-]+
\(user:
[0-9]"
|
tee
build-time.txt'
-
'
make
validate'
-
'
if
((
RANDOM
%
10
==
0
));
then
make
validate
;
fi
'
cache
:
key
:
"
coq8.6"
paths
:
...
...
Makefile
View file @
aad23129
...
...
@@ -32,9 +32,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
build-dep
:
build/opam-pins.sh < opam.pins
opam upgrade
$(YFLAG)
# it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
opam pin add
coq-stdp
p
"
$
$(pwd)
#HEAD"
-k
git
-n
-y
opam
install
coq-stdp
p
--deps-only
$(YFLAG)
opam pin remove
coq-stdp
p
opam pin add
opam-builddep-tem
p
"
$
$(pwd)
#HEAD"
-k
git
-n
-y
opam
install
opam-builddep-tem
p
--deps-only
$(YFLAG)
opam pin remove
opam-builddep-tem
p
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile
:
;
...
...
README.md
View file @
aad23129
...
...
@@ -18,7 +18,7 @@ The key features of this library are as follows:
`naive_solver`
, an equality simplifier
`simplify_eq`
, a solver
`solve_proper`
for proving compatibility of functions with respect to relations, and a solver
`set_solver`
for goals involving set operations.
-
It is entirely axiom
free.
-
It is entirely
dependency- and
axiom
-
free.
## History
...
...
@@ -32,8 +32,8 @@ developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
This version is known to compile with:
-
Coq 8.5pl3
and Coq
8.6
-
Coq 8.5pl3
/
8.6
## Building Instructions
Run
`make`
to build the full development.
Run
`make`
to build the full development.
Run
`make install`
to install the library.
build/opam-pins.sh
View file @
aad23129
...
...
@@ -4,18 +4,23 @@ set -e
## Usage:
## ./opam-pins.sh < opam.pins
if
!
which curl
>
/dev/null
;
then
echo
"opam-pins needs curl. Please install curl and try again."
exit
1
fi
# Process stdin
while
read
PACKAGE URL HASH
;
do
if
echo
"
$URL
"
| egrep
'^https://gitlab\.mpi-sws\.org'
>
/dev/null
;
then
echo
"[opam-pins] Recursing into
$URL
"
# an MPI URL -- try doing recursive pin processing
curl
-f
"
$URL
/raw/
$HASH
"
2>
/dev/null |
"
$0
"
curl
-f
"
$URL
/raw/
$HASH
/opam.pins
"
2>/dev/null |
"
$0
"
fi
if
opam pin list | fgrep
"
$PACKAGE
.dev.
$HASH
"
>
/dev/null
;
then
echo
"[opam-pins]
$PACKAGE
already at commit
$HASH
"
else
echo
"[opam-pins] Applying pin:
$PACKAGE
->
$URL
#
$HASH
"
opam pin add
"
$PACKAGE
.dev.
$HASH
"
"
$URL
#
$HASH
"
-k
git
-y
-n
echo
fi
echo
done
opam
View file @
aad23129
...
...
@@ -12,5 +12,5 @@ build: [
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/coq-stdpp'" ]
depends: [
"coq" { ((>= "8.
6
" & < "8.7~") | (= "dev"))}
"coq" { ((>= "8.
5.3
" & < "8.7~") | (= "dev"))}
]
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