Skip to content

Latest commit

 

History

History
116 lines (100 loc) · 7.38 KB

INSTRUCTORS.md

File metadata and controls

116 lines (100 loc) · 7.38 KB

Build instructions

Packages included

  • OCaml 4.14.0
  • opam 2.1.2
opam packages: ``` atd 2.12.0 Parser for the ATD data format description language atdgen 2.12.0 Generates efficient JSON serializers, deserializers and validators atdgen-runtime 2.12.0 Runtime library for code generated by atdgen atdts 2.12.0 TypeScript code generation for ATD APIs base v0.15.1 Full standard library replacement for OCaml base-bigarray base base-threads base base-unix base biniou 1.2.2 Binary data format designed for speed, safety, ease of use and backward compatible camlp-streams 5.0.1 The Stream and Genlex libraries for use with Camlp4 and Camlp5 cmdliner 1.2.0 Declarative definition of command line interfaces for OCaml conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.17.1 pinned to version 8.17.1 coq-bignums 9.0.0+coq8.17 Bignums, the Coq library of arbitrarily large numbers coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools coq-elpi 1.17.1 Elpi extension language for Coq coq-equations 1.3+8.17 A function definition package for Coq coq-ext-lib 0.11.8 A library of Coq definitions, theorems, and tactics coq-hierarchy-builder 1.4.0 High level commands to declare and evolve a hierarchy based on packed classes coq-mathcomp-ssreflect 2.0.0 Small Scale Reflection coq-quickchick 2.0.0 Randomized Property-Based Testing Plugin for Coq coq-serapi 8.17.0+0.17.0 Serialization library and protocol for machine interaction with the Coq proof as coq-simple-io 1.8.0 IO monad for Coq coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server cppo 1.6.9 Code preprocessor like cpp for OCaml csexp 1.5.2 Parsing and printing of S-expressions in Canonical form dune 3.9.1 pinned to version 3.9.1 dune-configurator 3.9.1 Helper library for gathering system configuration easy-format 1.3.4 High-level and functional interface to the Format module of the OCaml standard l elpi 1.16.10 ELPI - Embeddable λProlog Interpreter menhir 20230608 An LR(1) parser generator menhirLib 20230608 Runtime support library for parsers generated by Menhir menhirSdk 20230608 Compile-time library for auxiliary tools related to Menhir num 1.4 pinned to version 1.4 ocaml 4.14.1 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.1+options Official release of OCaml 4.14.1 ocamlbuild 0.14.2 OCamlbuild is a build system with builtin rules to easily build most OCaml projects ocamlfind 1.9.6 pinned to version 1.9.6 opam-depext 1.2.1-1 Install OS distribution packages parsexp v0.15.0 S-expression parsing library ppx_compare v0.15.0 Generation of comparison functions from types ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_deriving 5.2.1 Type-driven code generation for OCaml ppx_deriving_yojson 3.7.0 JSON codec generator for OCaml ppx_hash v0.15.0 A ppx rewriter that generates hash functions from type expressions and definitions ppx_import 1.10.0 A syntax extension for importing declarations from interface files ppx_sexp_conv v0.15.1 [@@deriving] plugin to generate S-expression conversion functions ppxlib 0.30.0 Standard infrastructure for ppx rewriters re 1.10.4 RE is a regular expression library for OCaml result 1.5 Compatibility Result module seq base Compatibility package for OCaml's standard iterator type starting from 4.07. sexplib v0.15.1 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.1.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 appropriate 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 customized by setting the COQ_IMAGE and OPAM_PACKAGES variables 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.