Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
75792e6a
Commit
75792e6a
authored
Jan 15, 2021
by
benoit
Browse files
remove coq
parent
caf9ce28
Changes
1000
Expand all
Hide whitespace changes
Inline
Side-by-side
Too many changes to show.
To preserve performance only
20 of 1000+
files are displayed.
Plain diff
Email patch
packages/coq/coq.8.8.2/.bintray.json
deleted
100644 → 0
View file @
caf9ce28
{
"package"
:
{
"name"
:
"coq"
,
"repo"
:
"coq"
,
"subject"
:
"coq"
},
"version"
:
{
"name"
:
"8.8.2"
},
"files"
:
[
{
"includePattern"
:
"_build/(.*
\\
.dmg)"
,
"uploadPattern"
:
"$1"
,
"matrixParams"
:
{
"override"
:
1
}
}
],
"publish"
:
true
}
packages/coq/coq.8.8.2/.github/ISSUE_TEMPLATE.md
deleted
100644 → 0
View file @
caf9ce28
<!-- Thank you for your contribution.
Please complete the following information when reporting a bug. -->
#### Version
<!-- You can get this information by running `coqtop -v`. -->
#### Operating system
#### Description of the problem
<!-- It is helpful to provide enough information so that we can reproduce the bug.
In particular, please include a code example which produces it.
If the example is small, you can include it here between
``` ```
.
Otherwise, please provide a link to a repository, a gist (https://gist.github.com)
or drag-and-drop a
`.zip`
archive. -->
packages/coq/coq.8.8.2/.github/PULL_REQUEST_TEMPLATE.md
deleted
100644 → 0
View file @
caf9ce28
<!-- Thank you for your contribution.
Make sure you read the contributing guide and fill this template. -->
<!-- Keep what applies -->
**Kind:**
documentation / bug fix / feature / performance / infrastructure.
<!-- If this is a bug fix, make sure the bug was reported beforehand. -->
Fixes / closes #????
<!-- If this is a feature pull request / breaks compatibility: -->
<!-- (Otherwise, remove these lines.) -->
-
[ ] Corresponding documentation was added / updated.
-
[ ] Entry added in CHANGES.
packages/coq/coq.8.8.2/.gitlab-ci.yml
deleted
100644 → 0
View file @
caf9ce28
image
:
"
$IMAGE"
stages
:
-
docker
-
build
-
test
# some default values
variables
:
# Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
# for reference]
CACHEKEY
:
"
bionic_coq-v8.8-V2018-09-20"
IMAGE
:
"
$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH
:
"
base"
# Used to select special compiler switches such as flambda, 32bits, etc...
OPAM_VARIANT
:
"
"
docker-boot
:
stage
:
docker
image
:
docker:stable
services
:
-
docker:dind
before_script
:
[]
script
:
-
docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
-
cd dev/ci/docker/bionic_coq/
-
if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
-
docker build -t "$IMAGE" .
-
docker push "$IMAGE"
except
:
variables
:
-
$SKIP_DOCKER == "true"
tags
:
-
docker
before_script
:
-
cat /proc/{cpu,mem}info ||
true
-
ls -a
# figure out if artifacts are around
-
printenv | sort
-
declare -A switch_table
-
switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" )
-
opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
-
eval $(opam config env)
-
opam list
-
opam config list
after_script
:
-
echo "The build completed normally (not a runner failure)."
################ GITLAB CACHING ######################
# - use artifacts between jobs #
######################################################
# TODO figure out how to build doc for installed Coq
.build-template
:
&build-template
stage
:
build
artifacts
:
name
:
"
$CI_JOB_NAME"
paths
:
-
_install_ci
-
config/Makefile
-
test-suite/misc/universes/all_stdlib.v
expire_in
:
1 week
script
:
-
set -e
-
echo 'start:coq.config'
-
./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
-
echo 'end:coq.config'
-
echo 'start:coq.build'
-
make -j "$NJOBS" byte
-
make -j "$NJOBS"
-
make test-suite/misc/universes/all_stdlib.v
-
echo 'end:coq:build'
-
echo 'start:coq.install'
-
make install
-
make install-byte
-
cp bin/fake_ide _install_ci/bin/
-
echo 'end:coq.install'
-
set +e
# every non build job must set dependencies otherwise all build
# artifacts are used together and we may get some random Coq. To that
# purpose, we add a spurious dependency `not-a-real-job` that must be
# overridden otherwise the CI will fail.
# set dependencies when using
.test-suite-template
:
&test-suite-template
stage
:
test
dependencies
:
-
not-a-real-job
script
:
-
cd test-suite
-
make clean
# careful with the ending /
-
BIN=$(readlink -f ../_install_ci/bin)/
-
LIB=$(readlink -f ../_install_ci/lib/coq)/
-
make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all
artifacts
:
name
:
"
$CI_JOB_NAME.logs"
when
:
on_failure
paths
:
-
test-suite/logs
# set dependencies when using
.validate-template
:
&validate-template
stage
:
test
dependencies
:
-
not-a-real-job
script
:
-
cd _install_ci
-
find lib/coq/ -name '*.vo' -print0 > vofiles
-
for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done
-
xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/
.ci-template
:
&ci-template
stage
:
test
script
:
-
set -e
-
echo 'start:coq.test'
-
make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET}
-
echo 'end:coq.test'
-
set +e
dependencies
:
-
build:base
variables
:
&ci-template-vars
TEST_TARGET
:
"
$CI_JOB_NAME"
.ci-template-flambda
:
&ci-template-flambda
<<
:
*ci-template
dependencies
:
-
build:edge+flambda
variables
:
<<
:
*ci-template-vars
OPAM_SWITCH
:
"
edge"
OPAM_VARIANT
:
"
+flambda"
.windows-template
:
&windows-template
stage
:
test
artifacts
:
name
:
"
%CI_JOB_NAME%"
paths
:
-
artifacts
when
:
always
expire_in
:
1 week
dependencies
:
[]
tags
:
-
windows
before_script
:
[]
script
:
-
call dev/ci/gitlab.bat
only
:
variables
:
-
$WINDOWS == "enabled"
build:base:
<<
:
*build-template
variables
:
COQ_EXTRA_CONF
:
"
-native-compiler
yes
-coqide
opt
-with-doc
yes"
# no coqide for 32bit: libgtk installation problems
build:base+32bit:
<<
:
*build-template
variables
:
OPAM_VARIANT
:
"
+32bit"
COQ_EXTRA_CONF
:
"
-native-compiler
yes"
build:edge:
<<
:
*build-template
variables
:
OPAM_SWITCH
:
edge
COQ_EXTRA_CONF
:
"
-native-compiler
yes
-coqide
opt"
build:edge+flambda:
<<
:
*build-template
variables
:
OPAM_SWITCH
:
edge
OPAM_VARIANT
:
"
+flambda"
COQ_EXTRA_CONF
:
"
-native-compiler
yes
-coqide
opt
-flambda-opts
"
COQ_EXTRA_CONF_QUOTE
:
"
-O3
-unbox-closures"
windows64
:
<<
:
*windows-template
variables
:
ARCH
:
"
64"
windows32
:
<<
:
*windows-template
variables
:
ARCH
:
"
32"
except
:
-
/^pr-.*$/
pkg:nix:
image
:
nixorg/nix:latest
# Minimal NixOS image which doesn't even contain git
stage
:
test
variables
:
# By default we use coq.cachix.org as an extra substituter but this can be overridden
EXTRA_SUBSTITUTERS
:
https://coq.cachix.org
EXTRA_PUBLIC_KEYS
:
coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI=
# The following variables should not be overridden
GIT_STRATEGY
:
none
CACHIX_PUBLIC_KEY
:
cachix.cachix.org-1:eWNHQldwUO7G2VkjpnjDbWwy4KQ/HNxht7H4SSoMckM=
NIXOS_PUBLIC_KEY
:
cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
dependencies
:
[]
# We don't need to download build artifacts
before_script
:
[]
# We don't want to use the shared 'before_script'
script
:
# Use current worktree as tmpdir to allow exporting artifacts in case of failure
-
export TMPDIR=$PWD
# Install Cachix as documented at https://github.com/cachix/cachix
-
nix-env -if https://github.com/cachix/cachix/tarball/master --substituters https://cachix.cachix.org --trusted-public-keys "$CACHIX_PUBLIC_KEY"
# We build an expression rather than a direct URL to not be dependent on
# the URL location; we are forced to put the public key of cache.nixos.org
# because there is no --extra-trusted-public-key option.
-
nix-build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}" -K --extra-substituters "$EXTRA_SUBSTITUTERS" --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS" | if [ ! -z "$CACHIX_SIGNING_KEY" ]; then cachix push coq; fi
artifacts
:
name
:
"
$CI_JOB_NAME.logs"
when
:
on_failure
paths
:
-
nix-build-coq.drv-0/*/test-suite/logs
test-suite:base:
<<
:
*test-suite-template
dependencies
:
-
build:base
test-suite:base+32bit:
<<
:
*test-suite-template
dependencies
:
-
build:base+32bit
variables
:
OPAM_VARIANT
:
"
+32bit"
test-suite:edge:
<<
:
*test-suite-template
dependencies
:
-
build:edge
variables
:
OPAM_SWITCH
:
edge
test-suite:edge+flambda:
<<
:
*test-suite-template
dependencies
:
-
build:edge+flambda
variables
:
OPAM_SWITCH
:
edge
OPAM_VARIANT
:
"
+flambda"
validate:base:
<<
:
*validate-template
dependencies
:
-
build:base
validate:base+32bit:
<<
:
*validate-template
dependencies
:
-
build:base+32bit
variables
:
OPAM_VARIANT
:
"
+32bit"
validate:edge:
<<
:
*validate-template
dependencies
:
-
build:edge
variables
:
OPAM_SWITCH
:
edge
validate:edge+flambda:
<<
:
*validate-template
dependencies
:
-
build:edge+flambda
variables
:
OPAM_SWITCH
:
edge
OPAM_VARIANT
:
"
+flambda"
ci-bedrock2
:
<<
:
*ci-template
ci-bignums
:
<<
:
*ci-template
ci-color
:
<<
:
*ci-template-flambda
ci-compcert
:
<<
:
*ci-template-flambda
ci-coq-dpdgraph
:
<<
:
*ci-template
ci-coquelicot
:
<<
:
*ci-template
ci-elpi
:
<<
:
*ci-template
ci-equations
:
<<
:
*ci-template
ci-fcsl-pcm
:
<<
:
*ci-template
ci-fiat-crypto
:
<<
:
*ci-template-flambda
ci-fiat-crypto-legacy
:
<<
:
*ci-template-flambda
ci-fiat-parsers
:
<<
:
*ci-template
ci-flocq
:
<<
:
*ci-template
ci-formal-topology
:
<<
:
*ci-template-flambda
ci-geocoq
:
<<
:
*ci-template-flambda
ci-hott
:
<<
:
*ci-template
ci-iris-lambda-rust
:
<<
:
*ci-template-flambda
ci-ltac2
:
<<
:
*ci-template
ci-math-comp
:
<<
:
*ci-template-flambda
ci-quickchick
:
<<
:
*ci-template-flambda
ci-mtac2
:
<<
:
*ci-template
ci-sf
:
<<
:
*ci-template
ci-unimath
:
<<
:
*ci-template-flambda
ci-vst
:
<<
:
*ci-template-flambda
packages/coq/coq.8.8.2/.travis.yml
deleted
100644 → 0
View file @
caf9ce28
dist
:
trusty
# Travis builds are slower using sudo: false (the container-based
# infrastructure) as of March 2017; see
# https://github.com/coq/coq/pull/467 for some discussion.
sudo
:
required
# Until Ocaml becomes a language, we set a known one.
language
:
c
cache
:
apt
:
true
directories
:
-
$HOME/.opam
before_cache
:
-
rm -rf ~/.opam/log/
addons
:
apt
:
sources
:
-
avsm
## Due to issues like
## https://github.com/travis-ci/travis-ci/issues/8507 ,
## https://github.com/travis-ci/travis-ci/issues/9000 ,
## https://github.com/travis-ci/travis-ci/issues/9081 , and
## https://github.com/travis-ci/travis-ci/issues/9126 , we get frequent
## failures with using `packages`. Therefore, for most targets, we
## instead invoke `apt-get update` manually with `travis_retry` before
## invoking `apt-get install`, manually, below in the `install:`
## target.
# packages:
# - opam
# - aspcud
# - gcc-multilib
env
:
global
:
-
NJOBS=2
# system is == 4.02.3
-
COMPILER="system"
-
COMPILER_BE="4.07.0"
-
DUNE_VER=".1.0.0"
-
CAMLP5_VER=".6.14"
-
CAMLP5_VER_BE=".7.06"
-
FINDLIB_VER=".1.4.1"
-
FINDLIB_VER_BE=".1.8.0"
-
LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2"
-
LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2"
-
NATIVE_COMP="yes"
-
COQ_DEST="-local"
-
MAIN_TARGET="world"
matrix
:
include
:
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="validate" TW="travis_wait"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="ci-coquelicot"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="ci-equations"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="ci-flocq"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="ci-hott"
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="ci-ltac2"
-
env
:
-
TEST_TARGET="lint"
install
:
[]
before_script
:
[]
addons
:
apt
:
sources
:
[]
packages
:
[]
script
:
-
dev/lint-repository.sh
# Full Coq test-suite with two compilers
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="sphinx test-suite"
-
EXTRA_CONF="-coqide opt"
-
EXTRA_OPAM="hevea ${LABLGTK}"
before_install
:
&sphinx-install
-
sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
addons
:
apt
:
sources
:
-
avsm
packages
:
&extra-packages
-
opam
-
aspcud
-
libgtk2.0-dev
-
libgtksourceview2.0-dev
-
python3
-
python3-pip
-
python3-setuptools
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="sphinx test-suite"
-
COMPILER="${COMPILER_BE}"
-
FINDLIB_VER="${FINDLIB_VER_BE}"
-
CAMLP5_VER="${CAMLP5_VER_BE}"
-
EXTRA_CONF="-coqide opt"
-
EXTRA_OPAM="hevea ${LABLGTK_BE}"
before_install
:
*sphinx-install
addons
:
apt
:
sources
:
-
avsm
packages
:
*extra-packages
# Full test-suite with flambda
-
if
:
NOT (type = pull_request)
env
:
-
TEST_TARGET="sphinx test-suite"
-
COMPILER="${COMPILER_BE}+flambda"
-
FINDLIB_VER="${FINDLIB_VER_BE}"
-
CAMLP5_VER="${CAMLP5_VER_BE}"
-
EXTRA_CONF="-coqide opt -flambda-opts -O3"
-
EXTRA_OPAM="hevea ${LABLGTK_BE}"
before_install
:
*sphinx-install
addons
:
apt
:
sources
:
-
avsm
packages
:
*extra-packages
-
os
:
osx
env
:
-
TEST_TARGET="test-suite"
-
COMPILER="${COMPILER_BE}"
-
FINDLIB_VER="${FINDLIB_VER_BE}"
-
CAMLP5_VER="${CAMLP5_VER_BE}"
-
NATIVE_COMP="no"
-
COQ_DEST="-local"
before_install
:
-
brew update
-
brew unlink python
-
brew install gnu-time
# only way to continue using OPAM 1.2
-
brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
-
if
:
NOT (type = pull_request)
os
:
osx
osx_image
:
xcode7.3
env
:
-
TEST_TARGET=""
-
COMPILER="${COMPILER_BE}"
-
FINDLIB_VER="${FINDLIB_VER_BE}"
-
CAMLP5_VER="${CAMLP5_VER_BE}"
-
NATIVE_COMP="no"
-
COQ_DEST="-prefix ${PWD}/_install"
-
EXTRA_CONF="-coqide opt -warn-error yes"
-
EXTRA_OPAM="${LABLGTK_BE}"
before_install
:
-
brew update
-
brew unlink python
-
brew install gnu-time gtk+ expat gtksourceview gdk-pixbuf
# only way to continue using OPAM 1.2
-
brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
-
brew unlink python@2
-
brew install python3
-
pip3 install macpack
before_deploy
:
-
dev/build/osx/make-macos-dmg.sh
deploy
:
-
provider
:
bintray
user
:
maximedenes
file
:
.bintray.json
key
:
secure
:
"
gUvXWwWR0gicDqsKOnBfe45taToSFied6gN8tCa5IOtl6E6gFoHoPZ83ZWXQsZP50oMDFS5eji0VQAFGEbOsGrTZaD9Y9Jnu34NND78SWL1tsJ6nHO3aCAoMpB0N3+oRuF6S+9HStU6KXWqgj+GeU4vZ4TOlG01RGctJa6U3vII="
skip_cleanup
:
true
on
:
all_branches
:
true
before_install
:
-
if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi
install
:
-
if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi
-
if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib --allow-unauthenticated; fi
-
opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
-
opam switch "$COMPILER" && opam update
-
eval $(opam config env)
-
opam config list
-
opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM}
-
opam list