Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update for Dune-Coq 0.8 and Coq 8.17 #7

Open
wants to merge 3 commits into
base: v8.16
Choose a base branch
from
Open

Update for Dune-Coq 0.8 and Coq 8.17 #7

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9d32950
update for Coq 8.17 and Dune-Coq 0.8
palmskog Jun 22, 2023
198e877
use docker-coq-action CI
palmskog Jun 22, 2023
bf2d563
update README.md, opam package and Docker CI
palmskog Jun 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 16 additions & 35 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,48 +1,29 @@
name: CI
name: Docker CI

on:
push:
branches:
- v8.16
- 'v8.17+0.8'
pull_request:
branches:
- v8.16

# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
- '**'

jobs:
build:
# the OS must be GNU/Linux to be able to use the docker-coq-action
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
ocaml-compiler: [4.09.x, 4.14.x]
coq-version: [8.16+rc1]
env:
NJOBS: "2"
OPAMJOBS: "2"
OPAMROOTISOK: "true"
OPAMYES: "true"
runs-on: ubuntu-latest

image:
- 'coqorg/coq:8.17'
fail-fast: false
steps:
- uses: actions/checkout@v2
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: avsm/setup-ocaml@v2
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}
dune-cache: true
- name: Install Coq
run: |
eval $(opam env)
opam repos add coq-released http://coq.inria.fr/opam/released
opam repos add coq-core-dev http://coq.inria.fr/opam/core-dev
opam install coq.${{ matrix.coq-version }}
- name: Display OPAM Setup
run: |
eval $(opam env)
opam list
- name: Test Template
run: |
eval $(opam env)
dune build --display=short
opam_file: 'coq-my-plugin.opam'
custom_image: ${{ matrix.image }}
before_install: |
startGroup "Print opam config and unpin dune"
opam config list; opam repo list; opam list; opam pin remove dune -y
endGroup
8 changes: 4 additions & 4 deletions coq-my-plugin.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ homepage: "https://github.com/your-github/my-plugin"
dev-repo: "git+https://github.com/your-github/my-plugin.git"
bug-reports: "https://github.com/your-github/my-plugin/issues"
doc: "https://your-github.github.io/my-plugin"
license: "MIT"
license: "SPDX-identifier-for-your-license"

synopsis: "One line description of your plugin"
description: """
Expand All @@ -14,9 +14,9 @@ cover multiple lines. Including punctuation."""

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
"ocaml" {>= "4.07.1"}
"dune" {>= "2.5"}
"coq" {>= "8.14" & < "8.15"}
"ocaml" {>= "4.09.0"}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe better to use a more recent OCaml version? I suggest 4.14.1

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But 4.14.1 isn't required, right? I thought we keep this the lower bound.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No it is not. That's a good question about what versions we put here. In general it will depend on the OCaml features the plugin writer uses.

Note also that 8.17.0 is not either a lower bound here, as the template works fine with 8.16.x

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As dicussed in Zulip, generally a template has a range of versions that it is suitable for, so we may want just to document the ranges users can do here.

  • In the case of Coq, for this version of the template >= 8.16 , tho it is trivial to adapt for 8.14, 8.15
  • In the case of OCaml, the bound is basically any OCaml in the 4.x series

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR doesn't work on Coq 8.16 since I removed -rectypes.

"dune" {>= "3.8.2"}
"coq" {>= "8.17"}
palmskog marked this conversation as resolved.
Show resolved Hide resolved
]

tags: [
Expand Down
4 changes: 2 additions & 2 deletions dune-project
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
(lang dune 2.9)
(using coq 0.3)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While we are at it we can use (generate_opam_files) and (opam_file_location)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem with opam file generation is that it brings another level of indirection. I think it's easier if we just keep the opam files manual...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Leaving the opam files manual is OK but has quite a few downsides too, in particular newer dune offers nice stuff if you declare the packages on dune-package, like source download, on top of the user having now to learn both opam syntax and dune syntax.

On other other hand, I can't see see any problem in the workflow with automatic file generation, what problems do you foresee? I don't understand what kind of indirection you refer to.

In fact the only reason that opam files need to be committed to the repository is due to "pinning", which is not yet smart enough to generate them on the fly. If you don't care about pinning you don't need to commit the .opam files and you can just ignore them, as dune-release will take care of properly generating them for repos upload.

(lang dune 3.8)
(using coq 0.8)
(name my-plugin)
12 changes: 4 additions & 8 deletions src/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,18 +10,14 @@

(synopsis "My Coq plugin") ; Synopsis, used in META generation.

(flags :standard -rectypes -w -27) ; Coq requires the `-rectypes`
; flag; CoqPP generated code
; requires to disable warning 27
; often.
(flags :standard -w -27) ; CoqPP generated code requires to
; disable warning 27 often.
palmskog marked this conversation as resolved.
Show resolved Hide resolved

(foreign_stubs ; we link our plugin with a C
(foreign_stubs ; We link our plugin with a C
(language c) ; library! Optional, of course.
(names ce_get))

(libraries ; OCaml Libraries we want to link
; with, your choice here.

(libraries ; OCaml libraries we want to link with
coq-core.vernac ; Needed for vernac extend.
coq-core.plugins.ltac ; Needed for tactic extend.
)
Expand Down
2 changes: 1 addition & 1 deletion theories/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
(package coq-my-plugin) ; Adding this line will make your
; library installable in the opam package

(libraries coq-my-plugin.plugin)) ; Here you should declare all
(plugins coq-my-plugin.plugin)) ; Here you should declare all
; OCaml plugin dependencies
; for your Coq files.

Expand Down