Skip to main content

Browse the archive

https://gitlab.com/nomadic-labs/mi-cho-coq
08 June 2021, 12:39:06 UTC
Revision 7a7a1aa403201894461c5ff40ae9fee67be399f3 authored by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC, committed by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC 
[michocoq] Redefine set.remove so that it computes
 
Before this commit, set.remove uses List.remove which only computes
when its decide_equality argument does. We passed it an opaque lemma
so it did not compute. Moreover, it always scanned the whole list but
since we only apply it on sorted lists it could stop as soon as it
encounters a value larger than the one to remove.

This commit redefines set.remove so that it does not depend on
decidability of equality anymore and returns as soon as it can.
1 parent 6406bf3
Raw File
Tip revision: 7a7a1aa403201894461c5ff40ae9fee67be399f3 authored by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC
[michocoq] Redefine set.remove so that it computes
Tip revision: 7a7a1aa
.gitlab-ci.yml 
stages:
  - lint
  # the build stage runs out-of-order w.r.t the lint stage as their is
  # no dependence. the separation is purely conceptual
  - build
  # the contracts stage depends only on michocoq:8.11 in the build
  # stage
  - contracts

lint:
  stage: lint
  image: alpine
  before_script:
    - apk --no-cache add emacs-nox
    - export scversion="latest"
    - wget -qO- "https://github.com/koalaman/shellcheck/releases/download/latest/shellcheck-"${scversion}".linux.x86_64.tar.xz" | tar -xJv
  script:
    - shellcheck-"${scversion}"/shellcheck `find -name 'configure'`
    - emacs --batch -l scripts/org-lint-README.el --kill

.build:
  stage: build
  # do not wait for lint
  needs: []
  before_script:
    - echo -e "section_start:`date +%s`:setup_switch\r\e[0K setup opam switch"
    - opam switch $COMPILER_EDGE; eval $(opam env)
    - echo -e "section_end:`date +%s`:setup_switch\r\e[0K"

    - echo -e "section_start:`date +%s`:setup_deps\r\e[0K setup the package dependencies"
    - opam update -y
    - sudo apt-get update -y -q
    - sudo chown -R coq:coq "$CI_PROJECT_DIR"
    - opam pin add -k git -y --no-action coq-mi-cho-coq .
    - opam depext -y coq-mi-cho-coq
    - echo -e "section_end:`date +%s`:setup_deps\r\e[0K"
  script:
    - echo -e "section_start:`date +%s`:project_build\r\e[0K build the project"
    # Use inplace build to get reusable build results
    - opam install -y --inplace-build -j ${NJOBS} --with-test coq-mi-cho-coq
    - echo -e "section_end:`date +%s`:project_build\r\e[0K"
    - which michocoq

michocoq:8.10:
  image: coqorg/coq:8.10
  extends: .build

michocoq:8.11:
  image: coqorg/coq:8.11
  extends: .build
  # pass built michocoq framework to contracts:8.11 job as artifacts
  # to speed up its build.
  artifacts:
    paths:
      - src/michocoq/*.vo
      - src/michocoq/micheline_parser.v
      - src/michocoq/extraction/_build

contracts:8.11:
  image: coqorg/coq:8.11
  extends: .build
  stage: contracts
  # only wait for michocoq:8.11
  needs:
    - michocoq:8.11
  script:
    - echo -e "section_start:`date +%s`:project_build\r\e[0K build the project"
    - opam install -y -j ${NJOBS} --deps-only coq-mi-cho-coq
    - echo -e "section_end:`date +%s`:project_build\r\e[0K"

    - echo -e "section_start:`date +%s`:check_contracts_coq\r\e[0K check contracts_coq"
    - ./configure contracts_coq
    - make
    - echo -e "section_end:`date +%s`:check_contracts_coq\r\e[0K"
back to top