Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487#!/usr/bin/env bash
# This is the list of repositories used by the CI scripts, unless overridden# by a call to the "overlay" function in ci-common
declare -a projects # the list of project repos that can be be overlayed
# checks if the given argument is a known projectfunction is_in_projects { for x in "${projects[@]}"; do if [ "$1" = "$x" ]; then return 0; fi; done return 1}
# project <name> <giturl> <ref> [<archiveurl>]# [<archiveurl>] defaults to <giturl>/archive on github.com# and <giturl>/-/archive on gitlabfunction project {
local var_ref=${1}_CI_REF local var_giturl=${1}_CI_GITURL local var_archiveurl=${1}_CI_ARCHIVEURL local giturl=$2 local ref=$3 local archiveurl=$4 case $giturl in *github.com*) archiveurl=${archiveurl:-$giturl/archive} ;; *gitlab*) archiveurl=${archiveurl:-$giturl/-/archive} ;; esac
# register the project in the list of projects projects[${#projects[*]}]=$1
# bash idiom for setting a variable if not already set : "${!var_ref:=$ref}" : "${!var_giturl:=$giturl}" : "${!var_archiveurl:=$archiveurl}"
}
# subproject <name> <parent project> <submodulefolder> <submodule giturl> <submodule branch># In the case of nested submodules, each subproject should be declared# a subproject of its immediate parent, to ensure overlays are applied# in the right orderfunction subproject { local var_parent_project=${1}_CI_PARENT_PROJECT local var_submodule_folder=${1}_CI_SUBMODULE_FOLDER local var_submodule_giturl=${1}_CI_SUBMODULE_GITURL local var_submodule_branch=${1}_CI_SUBMODULE_BRANCH local parent_project=$2 local submodule_folder=$3 local submodule_giturl=$4 local submodule_branch=$5
# register the project in the list of projects projects[${#projects[*]}]=$1
: "${!var_parent_project:=$parent_project}" : "${!var_submodule_folder:=$submodule_folder}" : "${!var_submodule_giturl:=$submodule_giturl}" : "${!var_submodule_branch:=$submodule_branch}"}
######################################################################### Micromega########################################################################project micromega "https://github.com/rocq-community/micromega-plugin" "master"# Contact @proux01 on github
######################################################################### MathComp########################################################################project mathcomp "https://github.com/math-comp/math-comp" "master"# Contact @CohenCyril, @proux01 on github
project fourcolor "https://github.com/math-comp/fourcolor" "master"# Contact @proux01 on github
project oddorder "https://github.com/math-comp/odd-order" "master"# Contact @gares, @proux01 on github
project mczify "https://github.com/math-comp/mczify" "master"# Contact @pi8027 on github
project finmap "https://github.com/math-comp/finmap" "master"# Contact @CohenCyril on github
project bigenough "https://github.com/math-comp/bigenough" "master"# Contact @CohenCyril on github
project analysis "https://github.com/math-comp/analysis" "master"# Contact @affeldt-aist, @CohenCyril on github
######################################################################### UniMath########################################################################project unimath "https://github.com/UniMath/UniMath" "master"# Contact @benediktahrens, @m-lindgren, @nmvdw, @rmatthes on github
######################################################################### Unicoq + Mtac2########################################################################project unicoq "https://github.com/unicoq/unicoq" "master"# Contact @Janno, @mattam82 on github
project mtac2 "https://github.com/Mtac2/Mtac2" "master"# Contact @Janno on github
######################################################################### Mathclasses + Corn########################################################################project math_classes "https://github.com/coq-community/math-classes" "master"# Contact @Lysxia and @spitters on github
project corn "https://github.com/coq-community/corn" "master"# Contact @Lysxia and @spitters on github
######################################################################### Iris########################################################################
# NB: stdpp and Iris refs are gotten from the opam files in the Iris and# iris_examples repos respectively. Those will be updated automatically within# 24h after a change lands in stdpp or Iris. Ping @RalfJung and @robbertkrebbers# if that does not work for some reason.# The URL below is a mirror; use https://gitlab.mpi-sws.org/iris/stdpp for issues# and PRs.project stdpp "https://github.com/rocq-iris/stdpp" ""# Contact @RalfJung, @robbertkrebbers on github
# The URL below is a mirror; use https://gitlab.mpi-sws.org/iris/iris for issues# and PRs.project iris "https://github.com/rocq-iris/iris" ""# Contact @RalfJung, @robbertkrebbers on github
project autosubst "https://github.com/coq-community/autosubst" "master"# Contact @RalfJung on github
# The URL below is a mirror; use https://gitlab.mpi-sws.org/iris/examples for# issues and PRs.project iris_examples "https://github.com/rocq-iris/examples" "master"# Contact @RalfJung, @robbertkrebbers on github
######################################################################### HoTT########################################################################project hott "https://github.com/HoTT/HoTT" "master"# Contact @Alizter, @jdchristensen on github
######################################################################### CoqHammer########################################################################project coqhammer "https://github.com/lukaszcz/coqhammer" "master"# Contact @lukaszcz on github
######################################################################### Flocq########################################################################project flocq "https://gitlab.inria.fr/flocq/flocq" "master"# Contact @silene on github
######################################################################### coq-performance-tests########################################################################project coq_performance_tests "https://github.com/coq-community/coq-performance-tests" "master"# Contact @JasonGross on github
######################################################################### coq-tools########################################################################project coq_tools "https://github.com/JasonGross/coq-tools" "master"# Contact @JasonGross on github
######################################################################### Coquelicot########################################################################project coquelicot "https://gitlab.inria.fr/coquelicot/coquelicot" "master"# Contact @silene on github
######################################################################### CompCert########################################################################project compcert "https://github.com/AbsInt/CompCert" "master"# Contact @xavierleroy on github
######################################################################### VST########################################################################project vst "https://github.com/PrincetonUniversity/VST" "master"# Contact @andrew-appel on github
######################################################################### rewriter########################################################################project rewriter "https://github.com/mit-plv/rewriter" "master"# Contact @JasonGross on github
######################################################################### fiat_parsers########################################################################project fiat_parsers "https://github.com/mit-plv/fiat" "master"# Contact @JasonGross on github
######################################################################### fiat_crypto_legacy########################################################################project fiat_crypto_legacy "https://github.com/mit-plv/fiat-crypto" "sp2019latest"# Contact @JasonGross on github
######################################################################### fiat_crypto########################################################################project fiat_crypto "https://github.com/mit-plv/fiat-crypto" "master"# Contact @andres-erbsen, @JasonGross on github
# bedrock2, coqutil, rupicola# fiat-crypto is not guaranteed to build with the latest version of# bedrock2, so we use the pinned version of bedrock2 for fiat-crypto# overlays do not have to follow suitesubproject rupicola fiat_crypto "rupicola" "https://github.com/mit-plv/rupicola" "master"subproject bedrock2 rupicola "bedrock2" "https://github.com/mit-plv/bedrock2" "master"subproject coqutil bedrock2 "deps/coqutil" "https://github.com/mit-plv/coqutil" "master"# Contact @samuelgruetter, @andres-erbsen on github
######################################################################### coq_dpdgraph########################################################################project coq_dpdgraph "https://github.com/coq-community/coq-dpdgraph" "coq-master"# Contact @Karmaki, @ybertot on github
######################################################################### CoLoR########################################################################project color "https://github.com/fblanqui/color" "master"# Contact @fblanqui on github
######################################################################### Bignums########################################################################project bignums "https://github.com/coq/bignums" "master"# Contact @erikmd, @proux01 on github
######################################################################### coqprime########################################################################project coqprime "https://github.com/thery/coqprime" "master"# Contact @thery on github
######################################################################### Coinduction########################################################################project coinduction "https://github.com/damien-pous/coinduction" "master"# Contact @damien-pous on github
######################################################################### rocq-extraction-scala########################################################################project rocq_extraction_scala "https://github.com/vbergeron/rocq-extraction-scala" "main"# Contact @vbergeron on github
######################################################################### rocq-lsp########################################################################project rocq_lsp "https://github.com/rocq-community/rocq-lsp" "main"# Contact @SkySkimmer on github
######################################################################### Equations########################################################################project equations "https://github.com/rocq-prover/equations" "main"# Contact @mattam82 on github
######################################################################### Elpi + Hierarchy Builder########################################################################project elpi "https://github.com/LPCIC/coq-elpi" "master"# Contact @gares on github
project hierarchy_builder "https://github.com/math-comp/hierarchy-builder" "master"# Contact @CohenCyril, @gares on github
######################################################################### Engine-Bench########################################################################project engine_bench "https://github.com/mit-plv/engine-bench" "master"# Contact @JasonGross on github
######################################################################### fcsl-pcm########################################################################project fcsl_pcm "https://github.com/imdea-software/fcsl-pcm" "master"# Contact @aleksnanevski, @clayrat on github
######################################################################### ext-lib########################################################################project ext_lib "https://github.com/coq-community/coq-ext-lib" "master"# Contact @liyishuai on github
######################################################################### simple-io########################################################################project simple_io "https://github.com/Lysxia/coq-simple-io" "master"# Contact @Lysxia, @liyishuai on github
######################################################################### quickchick########################################################################project quickchick "https://github.com/QuickChick/QuickChick" "master"# Contact @lemonidas, @Lysxia, @liyishuai on github
######################################################################### reduction-effects########################################################################project reduction_effects "https://github.com/coq-community/reduction-effects" "master"# Contact @liyishuai, @JasonGross on github
######################################################################### menhirlib######################################################################### Note: menhirlib is now in subfolder coq-menhirlib of menhirproject menhirlib "https://gitlab.inria.fr/fpottier/menhir" "master"# Contact @fpottier, @jhjourdan on github
######################################################################### coq-neural-net-interp########################################################################project neural_net_interp "https://github.com/JasonGross/neural-net-coq-interp" "tested"# Contact @JasonGross on github
######################################################################### aac_tactics########################################################################project aac_tactics "https://github.com/coq-community/aac-tactics" "master"# Contact @palmskog on github
######################################################################### paco########################################################################project paco "https://github.com/snu-sf/paco" "master"# Contact @damhiya on github
######################################################################### coq-itree########################################################################project itree "https://github.com/DeepSpec/InteractionTrees" "master"# Contact @Lysxia on github
######################################################################### paramcoq########################################################################project paramcoq "https://github.com/coq-community/paramcoq" "master"# Contact @ppedrot on github
######################################################################### relation_algebra########################################################################project relation_algebra "https://github.com/damien-pous/relation-algebra" "master"# Contact @damien-pous on github
######################################################################### Stdlib########################################################################project stdlib "https://github.com/coq/stdlib" "master"# Contact TODO on github
######################################################################### argosy########################################################################project argosy "https://github.com/mit-pdos/argosy" "master"# Contact @tchajed on github
######################################################################### ATBR########################################################################project atbr "https://github.com/coq-community/atbr" "master"# Contact @palmskog, @tchajed on github
######################################################################### metarocq########################################################################project metarocq "https://github.com/MetaRocq/metarocq" "main"# Contact @mattam82, @yforster on github
######################################################################### SF suite########################################################################project sf "https://github.com/DeepSpec/sf" "master"# Contact @bcpierce00, @liyishuai on github
######################################################################### Coqtail########################################################################project coqtail "https://github.com/whonore/Coqtail" "main"# Contact @whonore on github
######################################################################### Deriving########################################################################project deriving "https://github.com/arthuraa/deriving" "master"# Contact @arthuraa on github
######################################################################### VsRocq########################################################################project vsrocq "https://github.com/rocq-prover/vsrocq" "main"# Contact @rtetley, @gares on github
######################################################################### category-theory########################################################################project category_theory "https://github.com/jwiegley/category-theory" "master"# Contact @jwiegley on github
######################################################################### itauto########################################################################project itauto "https://gitlab.inria.fr/fbesson/itauto" "master"# Contact @fajb on github
######################################################################### Mathcomp-word########################################################################project mathcomp_word "https://github.com/jasmin-lang/coqword" "main"# Contact @vbgl, @strub on github
######################################################################### Jasmin########################################################################project jasmin "https://github.com/jasmin-lang/jasmin" "main"# Contact @vbgl, @bgregoir on github
######################################################################### Lean Importer########################################################################project lean_importer "https://github.com/coq-community/rocq-lean-import" "master"# Contact @SkySkimmer on github
######################################################################### SMTCoq########################################################################project smtcoq "https://github.com/smtcoq/smtcoq" "rocq-master"# Contact @ckeller on github
######################################################################### Stalmarck########################################################################project stalmarck "https://github.com/coq-community/stalmarck" "master"# Contact @palmskog on github
######################################################################### Tactician########################################################################project tactician "https://github.com/coq-tactician/coq-tactician" "coqdev"# Contact @LasseBlaauwbroek on github
######################################################################### Ltac2 compiler########################################################################project ltac2_compiler "https://github.com/SkySkimmer/coq-ltac2-compiler" "main"# Contact @SkySkimmer on github
######################################################################### Waterproof########################################################################project waterproof "https://github.com/impermeable/coq-waterproof" "coq-master"# Contact @jellooo038, @jim-portegies on github
######################################################################### Autosubst (2) OCaml########################################################################project autosubst_ocaml "https://github.com/uds-psl/autosubst-ocaml" "master"# Contact @yforster on github
######################################################################### Trakt########################################################################project trakt "https://github.com/rocq-trakt/trakt" "master"# Contact @ckeller, @lafeychine on github
######################################################################### MLtac2########################################################################project mltac2 "https://github.com/epfl-systemf/mltac2" "main"# Contact @dhalilov on github