Skip to main content

Browse the archive

Revision 83ca25b2d05918e2f5e1b28f25410d2e906ab42c authored by Dominique Larchey-Wendling on 19 April 2020, 16:08:37 UTC, committed by Dominique Larchey-Wendling on 19 April 2020, 16:08:37 UTC 
unified Vector.t and vec ... several problems.
 
1) vec_cons can no longer be used as a constructor
   but the notation _ ## _ can largely mitigate
2) Vector.cons X x n v = vec_cons X n x v ie the arguments
   are no in the same order. Ie when invoquing induction
   we explicit intro pattern, you need to rearrange arguments
3) default parameter names are diffents, typical v is replaced
   by t which means scripts that use autogenerated names will
   likely fail ...
1 parent 968ddf4
Raw File
.travis.yml 
dist: trusty
sudo: required
language: c
cache:
  apt: true
  directories:
  - $HOME/.opam
  - $HOME/bin
  
addons:
  apt:
    sources:
    - avsm
 
env:
  global:
  - NJOBS=2
  - COMPILER="4.07.1"
  matrix:
  - COQ_VER="8.11.0" EQUATIONS_VER="1.2.1+8.11" METACOQ_VER="1.0~alpha2+8.11" SMPL_VER="8.11" BASE_VER="1.0+8.11"
  
install:
- curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh > install.sh
- export PATH=$HOME/bin:$PATH
- which opam || (rm -rf $HOME/.opam; echo $HOME/bin | sudo sh install.sh --no-backup; opam init --disable-sandboxing -j ${NJOBS} --compiler=${COMPILER} -n -y)
- opam --version
- opam update
- opam init -j ${NJOBS} -n -y --compiler=$COMPILER
- opam switch set ${COMPILER}
- eval $(opam config env)
- opam config list
- opam repo add coq-released https://coq.inria.fr/opam/released || echo "coq-released registered"
- opam repo add psl-opam-repository https://github.com/uds-psl/psl-opam-repository.git || echo "psl-opam-repository registered"
- opam install -j ${NJOBS} -y coq.${COQ_VER} coq-equations.${EQUATIONS_VER} coq-metacoq-template.${METACOQ_VER} coq-metacoq-checker.${METACOQ_VER} coq-smpl.${SMPL_VER} coq-psl-base-library.${BASE_VER}
- opam list

script:
 - make -j ${NJOBS} all
back to top