Code

Experiment: Running Coq over IC.Ref#10

Code

Draft

nomeata wants to merge 20 commits intomasterdfinity/ic-hs:masterfrom hs-to-coqdfinity/ic-hs:hs-to-coqCopy head branch name to clipboard

+42,665-20

Commits

Commits on Mar 26, 2020

• stash

  Show description for 2b5a9c2
  nomeata

  committed
  2b5a9c2

  Copy full SHA for 2b5a9c2

Commits on Mar 27, 2020

• Use CPP to select Canister implementation

  Show description for f839015
  nomeata

  committed
  f839015

  Copy full SHA for f839015

• Nix setup

  Show description for 0e8249d
  nomeata

  committed
  0e8249d

  Copy full SHA for 0e8249d

Commits on Mar 28, 2020

• Make building hs-to-coq Hydra-friendly

  Show description for 9481765
  nomeata

  committed
  9481765

  Copy full SHA for 9481765

Commits on Mar 29, 2020

• Install coq libraries as intended

  Show description for 744f7fc
  nomeata

  committed
  744f7fc

  Copy full SHA for 744f7fc

• nix: Extract out ic-ref-ghc-env

  Show description for 9c292b0
  nomeata

  committed
  9c292b0

  Copy full SHA for 9c292b0

• Create a Makefile setup that works in nix-shell

  Show description for 2dcd00b
  nomeata

  committed
  2dcd00b

  Copy full SHA for 2dcd00b

• Begin a directory for the actual manual proofs

  Show description for f26f8f2
  nomeata

  committed
  f26f8f2

  Copy full SHA for f26f8f2

• Makefile cleanup

  Show description for 09e5e5b
  nomeata

  committed
  09e5e5b

  Copy full SHA for 09e5e5b

• More gitignore

  Show description for c66124d
  nomeata

  committed
  c66124d

  Copy full SHA for c66124d

• Actual proofs (random stashing)

  Show description for 17da077
  nomeata

  committed
  17da077

  Copy full SHA for 17da077

• Load base-thy

  Show description for fc3aa7b
  nomeata

  committed
  fc3aa7b

  Copy full SHA for fc3aa7b

• More Monad proofs

  Show description for b7cb1bc
  nomeata

  committed
  b7cb1bc

  Copy full SHA for b7cb1bc

• Try to unbreak ghc844 build on CI

  Show description for c7c4acc
  nomeata

  committed
  c7c4acc

  Copy full SHA for c7c4acc

• Use makeWrapper

  Show description for 43fd93a
  nomeata

  committed
  43fd93a

  Copy full SHA for 43fd93a

• Pass restricted evaluation

  Show description for 1ce38b0
  nomeata

  committed
  1ce38b0

  Copy full SHA for 1ce38b0

Commits on Mar 30, 2020

• Track nixpkgs master, my PR got merged

  Show description for c2bdd1a
  nomeata

  committed
  c2bdd1a

  Copy full SHA for c2bdd1a

• Checkpoint (machinery for reasoning about StateT and Except T)

  Show description for 8c4b4d9
  nomeata

  committed
  8c4b4d9

  Copy full SHA for 8c4b4d9

• Stash. Limits of SP known

  Show description for cdbfe4c
  nomeata

  committed
  cdbfe4c

  Copy full SHA for cdbfe4c

• More proofs

  Show description for 48280c0
  nomeata

  committed
  48280c0

  Copy full SHA for 48280c0