Skip to content

Commit

Permalink
CI: split Coq job
Browse files Browse the repository at this point in the history 
The coq-program job produces the extracted OCaml code in the CIL/
directory.

The coq-proof job checks all Coq proofs.

Also remove the redundant “dependencies” entries
  • Loading branch information
@vbgl
vbgl committed Mar 20, 2023
1 parent e9c5c83 commit 508eb67
Showing 1 changed file with 0 additions and 2 deletions.
2 changes: 0 additions & 2 deletions .gitlab-ci.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,6 @@ coq-program:
EXTRA_NIX_ARGUMENTS: --arg coqDeps true
extends: .common
script:
- nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs Makefile.coq'
- nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs -f Makefile.coq compiler/jasmin_compiler.vo'
- nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler CIL'
artifacts:
paths:
Expand Down

0 comments on commit 508eb67

Please sign in to comment.