Skip to content

Latest commit

 

History

History
101 lines (85 loc) · 5.97 KB

INSTRUCTORS.md

File metadata and controls

101 lines (85 loc) · 5.97 KB
Raw

Build instructions

Packages included

  • OCaml 4.14.0
  • opam 2.1.2
opam packages: ``` base v0.15.0 Full standard library replacement for OCaml base-bigarray base base-threads base base-unix base cmdliner 1.1.1 Declarative definition of command line interfaces for OCaml conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.15.2 pinned to version 8.15.2 coq-bignums 8.15.0 Bignums, the Coq library of arbitrary large numbers coq-equations 1.3+8.15 A function definition package for Coq coq-ext-lib 0.11.6 A library of Coq definitions, theorems, and tactics coq-mathcomp-ssreflect 1.14.0 Small Scale Reflection coq-quickchick dev pinned to version dev at git+https://github.com/QuickChick/QuickChick.git#a1522e07b01fcd948407a06726e49 coq-serapi 8.15.0+0.15.2 Serialization library and protocol for machine interaction with the Coq proof assistant coq-simple-io 1.7.0 IO monad for Coq cppo 1.6.9 Code preprocessor like cpp for OCaml csexp 1.5.1 Parsing and printing of S-expressions in Canonical form dune 3.3.1 pinned to version 3.3.1 dune-configurator 3.3.1 Helper library for gathering system configuration menhir 20220210 An LR(1) parser generator menhirLib 20220210 Runtime support library for parsers generated by Menhir menhirSdk 20220210 Compile-time library for auxiliary tools related to Menhir num 1.4 pinned to version 1.4 ocaml 4.14.0 The OCaml compiler (virtual package) ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged ocaml-config 2 OCaml Switch Configuration ocaml-option-flambda 1 Set OCaml to be compiled with flambda activated ocaml-variants 4.14.0+options Official release of OCaml 4.14.0 ocamlbuild 0.14.1 OCamlbuild is a build system with builtin rules to easily build most OCaml projects ocamlfind 1.9.1 pinned to version 1.9.1 opam-depext 1.2.1-1 Install OS distribution packages parsexp v0.15.0 S-expression parsing library ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_deriving 5.2.1 Type-driven code generation for OCaml ppx_deriving_yojson 3.6.1 JSON codec generator for OCaml ppx_import 1.9.1 A syntax extension for importing declarations from interface files ppx_sexp_conv v0.15.0 [@@deriving] plugin to generate S-expression conversion functions ppxlib 0.25.1 Standard library for ppx rewriters result 1.5 Compatibility Result module seq base Compatibility package for OCaml's standard iterator type starting from 4.07. sexplib v0.15.0 Library for serializing OCaml values to and from S-expressions sexplib0 v0.15.1 Library containing the definition of S-expressions and some base converters stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler yojson 2.0.0 Yojson is an optimized parsing and printing library for the JSON format zarith 1.12 pinned to version 1.12 ```

Build and deploy Docker image

The prebuilt Docker image can be found on Docker Hub. You can build the image yourself using the following command. Replacing IMAGE_NAME and TAG with appropiate values.

docker build src -t IMAGE_NAME:TAG

By default this will build a Docker image identical to the prebuilt image. See what is included in the image here.

The image can be qustomized by setting the COQ_IMAGE and OPAM_PACKAGES variable as shown below:

docker build src -t IMAGE_NAME:TAG --build-arg COQ_IMAGE=X OPAM_PACKAGES=Y
  • COQ_IMAGE: The base image which has OCaml and Coq installed. Use images from coqorg
  • OPAM_PACKAGES: The opam packages installed in the image

Building the image can take a while.

The following commands will push the image to Docker Hub

docker login
docker tag IMAGE_NAME:TAG DOCKER_HUB_USERNAME/IMAGE_NAME:TAG
docker push DOCKER_HUB_USERNAME/IMAGE_NAME:TAG

After pushing the image the .devcontainer.json file will need to be updated. Update the line "image": "eskehoy/aufsv22:latest" to reflect the username, image name and tag used above. The tag can be omitted, in which case VSCode will always pull the latest tag.

If the devcontainer is used with a project containing a _CoqProject file, the file must be located in the project root. If not the "coq.coqProjectRoot": "." line must be updated to tell Coq where the _CoqProject file is located.

Customize devcontainer file

The .devcontainer.json file is made up of three different components:

  • The image that VSCode will use
  • A list of VSCode extensions to install
  • A list of VSCode options

The image used by default is the latest tag of the eskehoy/aufsv22 Docker Hub image.

By default the VsCoq extension will be installed in the devcontainer.

The default settings defined in .devcontainer.json will hide compiled Coq files in the file explorer, and set the default tab size to 2 spaces in Coq files. Additional settings can be added here.