Enable track test suite

Bubbler-4 commented 5 years ago

After some experiments, I got a nice way for track testing without a complex shell(or python or whatever) script. Still need to figure out if it works on deployment (CI + docker and, of course, the site).

(Side note: I don't think Print Assumptions is necessary at all; equality tests and type checks should suffice. The command has been used for automatic checking, but if a student tries to use an axiom in any way, it's highly visible in the code itself. Also, some useful packages naturally introduce a few axioms such as functional extensionality or proof irrelevance, and real numbers are made up upon a collection of axioms. Using Print Assumptions on them would give noisy outputs on the console, possibly confusing the student.

Btw, Codewars solved the axioms problem by creating a mini testing framework as an ML module, but I guess such a thing isn't a particularly good fit for Exercism.)

To-do list

[ ] Change the filenames on the exercises to *Defs.v, *.v, *Test.v, example/*.v
[ ] Add Makefile and _CoqProject to each exercise
[ ] Add make in the Travis script
[ ] Make sure the existing exercises have proper contents and pass the track tests
[ ] Update test_pattern, ignore_pattern, solution_pattern in config.json as per the docs
[ ] Check that the exercises are deployed correctly on the main site (is there a way to check this before actual deployment?)
[ ] Update README to reflect the track test command
[ ] Update the template for students view
[ ] Add the generation tool

Testing setup for single exercise

Directory structure

hello-world
- HelloWorldDefs.v : Preliminary definitions
- HelloWorld.v : Exercise tasks
- HelloWorldTest.v : Type checking scripts
- _CoqProject : Lets CoqIde/ProofGeneral detect dependencies
- Makefile : Build scripts
- example
  - HelloWorld.v : Reference solution

`HelloWorldDefs.v`

From Coq Require Export String.

`HelloWorld.v`

From HelloWorld Require Import HelloWorldDefs.

Definition hello_world : string. Admitted.

`HelloWorldTest.v`

From HelloWorld Require Import HelloWorldDefs HelloWorld.

Example test : hello_world = "Hello, World!"%string.
Proof. reflexivity. Qed.

`example/HelloWorld.v`

From HelloWorld Require Import HelloWorldDefs.

Definition hello_world : string := "Hello, World!".

`_CoqProject`

-R . HelloWorld

HelloWorldDefs.v
HelloWorld.v
example/HelloWorld.v
HelloWorldTest.v

`Makefile`

.PHONY: check track clean

NAME=HelloWorld
COQC=coqc -R . $(NAME)

check:
    $(COQC) $(NAME)Defs.v
    $(COQC) $(NAME).v
    $(COQC) $(NAME)Test.v

track:
    $(COQC) $(NAME)Defs.v
    $(COQC) example/$(NAME).v -o $(NAME).vo
    $(COQC) $(NAME)Test.v

clean:
    rm -f *.vo *.glob

Instructions for students

Run make check once before opening the IDE. Otherwise the *Defs module is not detected.
After completing the definitions/proofs, run make check to check for compilation errors.
If it compiles without any error, congratulations, you're good to go.
Run make clean to remove artifacts.

Track test instructions

Run make track to compile with reference solution.

Track test setup for multiple exercises

Directory structure

exercism
- Makefile
- exercises
  - hello-world
    - ... (as shown above, including its own makefile)
  - rna-transcription
    - ...

Top level `Makefile`

SUBDIRS := $(patsubst exercises/%/.,%,$(wildcard exercises/*/.))
.PHONY: all clean $(SUBDIRS)

all: $(SUBDIRS)
$(SUBDIRS):
    $(MAKE) -C exercises/$@ track

clean:
    find . -regextype posix-egrep -regex '.*\.(vo|glob)' -delete

Track test instructions

Run make to run (build) track tests for all exercises.
Run make <exercise-folder-name> to run the track test for a specific exercise.
- For multiple exercises, make <ex1> <ex2>.
If make succeeds, the exercises are ready.
Run make clean to clean all build artifacts.

Bubbler-4 commented 5 years ago

I'm planning to apply the changes in two phases:

Update existing exercises' filenames to meet the format above, and update test_pattern, ignore_pattern, solution_pattern in config.json as per the docs, and see if the exercises are deployed correctly on the main site
Add Makefiles and a make command in Travis script, and update README accordingly

I guess I could also make a template (or a script) that generates a new exercise with the same format.

Related: #3 #21 #6 #2

Bubbler-4 commented 5 years ago

This should do for the generation script.

#!/bin/bash
# $1 = folder name
# $2 = main module name

if [ $# == 2 ]; then
  cd exercises
  mkdir "$1"
  cd "$1"
  echo "(* TODO: Add preliminary definitions. *)" > "$2Defs.v"
  echo "From $2 Require Import $2Defs.

(* TODO: Add exercise skeletons. *)" > "$2.v"
  echo "From $2 Require Import $2Defs $2.

(* TODO: Add test cases. *)" > "$2Test.v"
  echo ".PHONY: check track clean

NAME=$2
COQC=coqc -R . \$(NAME)

check:
    \$(COQC) \$(NAME)Defs.v
    \$(COQC) \$(NAME).v
    \$(COQC) \$(NAME)Test.v

track:
    \$(COQC) \$(NAME)Defs.v
    \$(COQC) example/\$(NAME).v -o \$(NAME).vo
    \$(COQC) \$(NAME)Test.v

clean:
    rm -f *.vo *.glob" > Makefile
  echo "-R . $2

$2Defs.v
$2.v
example/$2.v
$2Test.v" > "_CoqProject"
  mkdir example
  cd example
  echo "From $2 Require Import $2Defs.

(* TODO: Add reference solution. *)" > "$2.v"
  cd ../../..
else
  echo "Usage: gen.sh <folder_name> <module_name>"
fi

NobbZ commented 5 years ago

I can help you with CI if that's a missing piece, I won't be able to do so before next weekend. Could you please write up some instructions how to get coq up and running on an Ubuntu Linux?

If docker is easier I can get that running two, but that would take me another day to figure out the details about docker on Travis.

Bubbler-4 commented 5 years ago

@NobbZ The easiest way to use Coq would be to use the official Coq docker image.

Installing natively on Ubuntu had some problems around opam 2 and bubblewrap. My workaround was to install opam via apt-get (this installs opam 1.2) and follow the previous instruction for Coq 8.9.0. The caveat is that you only get 8.9.0 while the latest stable is 8.9.1.

Full instruction:

Run the following script

# I don't recall all of the necessary dependencies, but here are at least some of them
sudo apt-get install opam m4 libgtksourceview2.0-dev 
export OPAMROOT=~/opam-coq.8.9.0
opam init -n --comp 4.02.3
opam repo add coq-released http://coq.inria.fr/opam/released
opam install coq.8.9.0 && opam pin add coq 8.9.0
opam install coqide # if you want an IDE

Add the following to .bashrc or equivalent

export OPAMROOT=~/opam-coq.8.9.0
eval `opam config env`

But in case you didn't notice, I already got the CI running with Coq docker, though Travis seems to fetch the image every time it runs (which takes over a minute, and IIRC the docs say we can't cache it).

The only question right now is, do the *_pattern options operate on full paths or individual filenames? (I saw the comments on Slack but forgot to ask this.)

NobbZ commented 5 years ago

Caching would be possible by some tricks, but that wouldn't change anything, perhaps even slow things down, as docker only downloads image, but if we were caching (using load and save of docker) we would add additional upload and compression steps for the cached artifact.

Also one minute of downloading the image is probably father than bootstrapping the VM each time from scratch.

Anyway I'm looking forward to see what you make from coq, as coq, Idris, agda and similar languages are interesting to me, but I rarely have possibility to use them.

exercism / coq