-
Notifications
You must be signed in to change notification settings - Fork 10
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Uses Docker-Coq-Action and the Coq-community templates to generate the configuration.
- Loading branch information
Showing
3 changed files
with
106 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,48 @@ | ||
name: Docker CI | ||
|
||
on: | ||
push: | ||
branches: | ||
- main | ||
pull_request: | ||
branches: | ||
- '**' | ||
|
||
jobs: | ||
build: | ||
# the OS must be GNU/Linux to be able to use the docker-coq-action | ||
runs-on: ubuntu-latest | ||
steps: | ||
- uses: actions/checkout@v4 | ||
- uses: coq-community/docker-coq-action@v1 | ||
with: | ||
opam_file: 'coq-platform-docs.opam' | ||
before_script: | | ||
startGroup "Workaround permission issue" | ||
sudo chown -R coq:coq . # <-- | ||
endGroup | ||
startGroup "Install npm" | ||
# installs nvm (Node Version Manager) | ||
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.7/install.sh | bash | ||
# download and install Node.js (you may need to restart the terminal) | ||
nvm install 20 | ||
# verifies the right Node.js version is in the environment | ||
node -v # should print `v20.14.0` | ||
# verifies the right NPM version is in the environment | ||
npm -v # should print `10.7.0` | ||
endGroup | ||
script: | | ||
startGroup "Build" | ||
cd src | ||
make node_modules | ||
make | ||
endGroup | ||
uninstall: "" | ||
|
||
|
||
# See also: | ||
# https://github.com/coq-community/docker-coq-action#readme | ||
# https://github.com/erikmd/docker-coq-github-action-demo |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
# This file was generated from `meta.yml`, please do not edit manually. | ||
# Follow the instructions on https://github.com/coq-community/templates to regenerate. | ||
|
||
opam-version: "2.0" | ||
maintainer: "Théo Zimmermann <[email protected]>" | ||
version: "dev" | ||
|
||
homepage: "https://github.com/Zimmi48/platform-docs" | ||
dev-repo: "git+https://github.com/Zimmi48/platform-docs.git" | ||
bug-reports: "https://github.com/Zimmi48/platform-docs/issues" | ||
|
||
|
||
synopsis: "A project of short tutorials and how-to guides for Coq features and Coq Platform packages." | ||
description: """ | ||
This project aims to create an online compilation of short and interactive tutorials and how-to guides for Coq and the Coq Platform. | ||
|
||
Each core functionality and plugin of Coq and the Coq Platform should have (short) pedagogical tutorials and/or how-to guides demonstrating how to use the functionality, with practical examples. They should further be available online through an interactive interface, most likely using JSCoq. | ||
|
||
Tutorials and how-to guides serve different purposes and are complementary. Tutorials guide a user during learning in discovering specific aspects of a feature like "Notations in Coq", by going through (simple) predetermined examples, and introducing notions gradually. In contrast, how-to guides are use-case-oriented and guides users through real life problems and their inherent complexity, like "How to define functions by well-founded recursion and reason about them". | ||
""" | ||
|
||
build: [make "-j%{jobs}%"] | ||
install: [make "install"] | ||
depends: [ | ||
"coq" | ||
"coq-equations" | ||
] | ||
|
||
tags: [ | ||
"logpath:" | ||
] | ||
authors: [ | ||
"Thomas Lamiaux" | ||
"Pierre Rousselin" | ||
"Théo Zimmermann" | ||
] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
fullname: "Coq Platform Docs" | ||
shortname: platform-docs | ||
organization: Zimmi48 # To change later to "coq" | ||
synopsis: "A project of short tutorials and how-to guides for Coq features and Coq Platform packages." | ||
description: | | ||
This project aims to create an online compilation of short and interactive tutorials and how-to guides for Coq and the Coq Platform. | ||
Each core functionality and plugin of Coq and the Coq Platform should have (short) pedagogical tutorials and/or how-to guides demonstrating how to use the functionality, with practical examples. They should further be available online through an interactive interface, most likely using JSCoq. | ||
Tutorials and how-to guides serve different purposes and are complementary. Tutorials guide a user during learning in discovering specific aspects of a feature like "Notations in Coq", by going through (simple) predetermined examples, and introducing notions gradually. In contrast, how-to guides are use-case-oriented and guides users through real life problems and their inherent complexity, like "How to define functions by well-founded recursion and reason about them". | ||
authors: | ||
- name: "Thomas Lamiaux" | ||
- name: "Pierre Rousselin" | ||
- name: "Théo Zimmermann" | ||
# TODO: add license | ||
dependencies: | ||
- description: Equations | ||
opam: | ||
name: coq-equations | ||
opam-file-maintainer: "Théo Zimmermann <[email protected]>" | ||
tested_coq_opam_versions: | ||
- version: "8.19" |