jtpaasch

Coq Dockerfiles

These are just experiments. Turns out the ocaml/opam docker containers only use a local copy of the opam repo, so opam update does nothing. Consequently, opam install coq.8.8.1 (for instance) would always say No such package. After I learned that I simply needed to add a remote opam repository to the docker container, regular opam install X started to work again, so my docker files got simpler.

I'm putting these here just to save them somewhere. There are little

jtpaasch

(** * Poly: Polymorphism and Higher-Order Functions *)

(* Final reminder: Please do not put solutions to the exercises in
   publicly accessible places.  Thank you!! *)

(* Suppress some annoying warnings from Coq: *)
Set Warnings "-notation-overridden,-parsing".
Require Export Lists.

(* ################################################################# *)

jtpaasch

(** * Induction: Proof by Induction *)

(** Before getting started, we need to import all of our
    definitions from the previous chapter: *)

Require Export Basics.

(** For the [Require Export] to work, you first need to use
    [coqc] to compile [Basics.v] into [Basics.vo].  This is like
    making a [.class] file from a [.java] file, or a [.o] file from a

jtpaasch

(** * Lists: Working with Structured Data *)

Require Export Induction.
Module NatList.

(* ################################################################# *)
(** * Pairs of Numbers *)

(** In an [Inductive] type definition, each constructor can take
    any number of arguments -- none (as with [true] and [O]), one (as

jtpaasch

(** * Basics: Functional Programming in Coq *)

(* REMINDER:

          #####################################################
          ###  PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY  ###
          #####################################################

   (See the [Preface] for why.)
*)

jtpaasch

(* CLI =============================== *)

let pid_value = ref (-1)
let get_pid () = !pid_value

let check () =
  match get_pid () with
  | (-1) ->
    Printf.printf "Error. Please provide a PID.\n%!";
    exit 1

jtpaasch

OCaml Projects

Simple project

Create a folder called myutility, with a Makefile, as well as a src subfolder:

mkdir ~/myutility

jtpaasch

OCaml Systems Programming

Including the unix module

To compile

Compile your modules first, e.g.:

jtpaasch

(* A utility for building a table that can be printed on a TTY.
   Use it by calling [create], and passing it a list of string lists.
   The argument is a list of rows, where each row is a list of strings.
   The [create] function returns a string you can print to a TTY. *)

let rec longest items res =
  match items with
  | [] -> res
  | hd :: tl ->
    match hd > res with

jtpaasch

module Tty_str = struct

  type ttyfmt =
    | Plain
    | Red
    | Green
    | Yellow
    | Bold
    | Dim
    | Italic