Experiment: Running Coq over IC.Ref

default.nix

@@ -32,6 +32,147 @@ let haskellPackages = nixpkgs.haskellPackages.override {
   overrides = import nix/haskell-packages.nix nixpkgs subpath;
 }; in
 
+
+let hs-to-coq-pkgs = nixpkgs.haskell.packages."lts-12.26"; in
+let hs-to-coq-unwrapped = hs-to-coq-pkgs.callPackage nix/generated/hs-to-coq.nix {}; in
+
+# running hs-to-coq requires loading files into GHC-the-library
+# so we need the dependencies available. This derivation
+# builds the appropriate package data base
+let
+  ic-ref-ghc-env = nixpkgs.runCommandNoCC "ic-ref-ghc-env" {
+    nativeBuildInputs = [ hs-to-coq-pkgs.ghc ];
+  } ''
+    packageConfDir="$out"
+    mkdir -p $packageConfDir
+    cp -f "${hs-to-coq-pkgs.memory}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    cp -f "${hs-to-coq-pkgs.basement}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    cp -f "${hs-to-coq-pkgs.cryptonite}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    cp -f "${nixpkgs.haskell.packages.ghc844.primitive}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    cp -f "${nixpkgs.haskell.packages.ghc844.vector}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    cp -f "${nixpkgs.haskell.packages.ghc844.base16-bytestring}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    cp -f "${nixpkgs.haskell.packages.ghc844.hex-text}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    cp -f "${nixpkgs.haskell.lib.markUnbroken (nixpkgs.haskell.lib.dontCheck nixpkgs.haskell.packages.ghc844.crc)}/lib/${hs-to-coq-pkgs.ghc.name}/package.conf.d/"*.conf $packageConfDir/
+    ghc-pkg --package-conf="$packageConfDir" recache
+    GHC_PACKAGE_PATH=$packageConfDir: ghc-pkg check
+  '';
+
+  hs-to-coq = stdenv.mkDerivation {
+    name = "hs-to-coq";
+    buildInputs = [ nixpkgs.makeWrapper ];
+    phases = [ "buildPhase" "fixupPhase" ];
+    setupHook = nixpkgs.writeText "setupHook.sh" ''
+      addHsToCoqPath () {
+        if test -d "''$1/lib/hs-to-coq"; then
+          export HS_TO_COQ_ARGS="''${HS_TO_COQ_ARGS-}''${HS_TO_COQ_ARGS:+ }--iface-dir=''$1/lib/hs-to-coq/"
+        fi
+        if test -e "''$1/lib/hs-to-coq/edits"; then
+          export HS_TO_COQ_ARGS="''${HS_TO_COQ_ARGS-}''${HS_TO_COQ_ARGS:+ }-e ''$1/lib/hs-to-coq/edits"
+        fi
+      }
+      addEnvHooks "$targetOffset" addHsToCoqPath
+    '';
+    buildPhase = ''
+      makeWrapper ${hs-to-coq-unwrapped}/bin/hs-to-coq $out/bin/hs-to-coq \
+        --unset NIX_GHCPKG \
+        --unset NIX_GHC_LIBDIR \
+        --unset NIX_GHC_DOCDIR \
+        --unset NIX_GHC \
+        --set GHC_PACKAGE_PATH "${ic-ref-ghc-env}:" \
+        --add-flags \$HS_TO_COQ_ARGS
+    '';
+  };
+
+  mkHsToCoqLib = name: src: subpath: stdenv.mkDerivation {
+    name = name;
+    src = src;
+    phases = [ "unpackPhase" "installPhase" ];
+    installPhase = ''
+      cd ${subpath}
+      mkdir -p $out/lib/hs-to-coq/
+      shopt -s globstar
+      cp --parents --dereference --target-directory=$out/lib/hs-to-coq **/*.h2ci
+      if test -e edits; then cp --dereference edits $out/lib/hs-to-coq; fi
+    '';
+  };
+
+  hs-to-coq-base = mkHsToCoqLib "base" nixpkgs.sources.hs-to-coq "base";
+  hs-to-coq-transformers = mkHsToCoqLib "transformers" nixpkgs.sources.hs-to-coq "examples/transformers/lib";
+  hs-to-coq-containers = mkHsToCoqLib "containers" nixpkgs.sources.hs-to-coq "examples/containers/lib";
+
+  ic-ref-coq-files = stdenv.mkDerivation {
+    name = "ic-ref-coq-files";
+    nativeBuildInputs = [
+      hs-to-coq-pkgs.ghc hs-to-coq
+      hs-to-coq-base hs-to-coq-transformers hs-to-coq-containers
+    ];
+    src = subpath ./proofs;
+    buildPhase = ''
+      mkdir -p $out
+      LANG=C.UTF8 SRC=${subpath impl/src} make vfiles
+      test -e lib/IC/Ref.v # sanity check
+    '';
+    installPhase = ''
+      cp -r lib/* $out
+    '';
+  };
+
+  mkCoqLib = { name, src, prefix ? "\"\"", subdir ? ".", delete ? [], deps ? [] }:
+   stdenv.mkDerivation {
+    name = "coq${nixpkgs.coq.coq-version}-${name}";
+    inherit src;
+    preBuild = ''
+      cd ${subdir}
+      echo '-Q . ${prefix}' > _CoqProject
+      rm -f ${nixpkgs.lib.concatStringsSep " " delete}
+      find -name \*.v >> _CoqProject
+      coq_makefile -f _CoqProject -o Makefile
+    '';
+    buildInputs = [ nixpkgs.coq ] ++ deps;
+    installFlags = "COQLIB=$(out)/lib/coq/${nixpkgs.coq.coq-version}/";
+    meta = { description = "hs-to-coq coq library ${name}"; };
+  };
+
+  coq-base = mkCoqLib {
+    name = "base";
+    src = nixpkgs.sources.hs-to-coq;
+    subdir = "base";
+    delete = ["Data/Char.v"];
+  };
+  coq-base-thy = mkCoqLib {
+    name = "base-thy";
+    src = nixpkgs.sources.hs-to-coq;
+    subdir = "base-thy";
+    deps = [ coq-base ];
+    prefix = "Proofs";
+  };
+  coq-transformers = mkCoqLib {
+    name = "transformers";
+    src = nixpkgs.sources.hs-to-coq;
+    subdir = "examples/transformers/lib";
+    deps = [ coq-base ];
+  };
+  coq-containers = mkCoqLib {
+    name = "containers";
+    src = nixpkgs.sources.hs-to-coq;
+    subdir = "examples/containers/lib";
+    deps = [ coq-base ];
+    delete = ["Data/SequenceManual.v"];
+  };
+  coq-ic-ref = mkCoqLib {
+    name = "ic-ref";
+    src = ic-ref-coq-files;
+    deps = [ coq-base coq-transformers coq-containers ];
+  };
+  coq-ic-ref-theories = mkCoqLib {
+    name = "ic-ref-theories";
+    src = subpath proofs/theories;
+    deps = [ coq-base coq-transformers coq-containers coq-ic-ref coq-base-thy ];
+    prefix = "Proofs";
+  };
+in
+
+
 let ic-ref = haskellPackages.ic-ref.overrideAttrs (old: {
   installPhase = (old.installPhase or "") + ''
     cp -rv test-data $out/test-data
@@ -48,6 +189,12 @@ rec {
   inherit ic-ref;
   inherit ic-ref-coverage;
   inherit universal-canister;
+  inherit hs-to-coq;
+  inherit ic-ref-ghc-env;
+  inherit ic-ref-coq-files;
+  inherit coq-ic-ref;
+  inherit coq-ic-ref-theories;
+  inherit hs-to-coq-base;
 
   ic-ref-test = nixpkgs.runCommandNoCC "ic-ref-test" {
       nativeBuildInputs = [ ic-ref nixpkgs.wabt ];
@@ -157,7 +304,15 @@ rec {
       nixpkgs.ghcid
     ] ++
     # and to build the rust stuff
-    universal-canister.nativeBuildInputs; in
+    universal-canister.nativeBuildInputs ++
+    # and a bunch of coq stuff
+    [ nixpkgs.coq
+      coq-base coq-containers coq-transformers
+      coq-base-thy
+      hs-to-coq
+      hs-to-coq-base hs-to-coq-transformers hs-to-coq-containers
+    ]
+    ; in
 
     haskellPackages.ic-ref.env.overrideAttrs (old: {
       nativeBuildInputs = (old.nativeBuildInputs or []) ++ extra-pkgs ;

ic-ref.cabal

@@ -17,6 +17,10 @@ flag release
 --
 -- > cabal: Cannot open a repl for multiple components at once.
 
+flag canister-persisted
+  default: True
+  manual: True
+
 common version
   hs-source-dirs:      src
   other-modules:       IC.Version
@@ -39,7 +43,7 @@ common logic
   other-modules:       IC.Wasm.WinterMemory
   other-modules:       IC.Wasm.Winter.Persist
   other-modules:       IC.Wasm.Imports
-  build-depends:       base >=4.13 && <5
+  build-depends:       base
   build-depends:       filepath
   build-depends:       hex-text
   build-depends:       crc
@@ -58,6 +62,11 @@ common logic
   build-depends:       cryptonite
   build-depends:       memory
 
+  if flag(canister-persisted)
+    cpp-options: -DCANISTER_PERSISTED
+  else
+    cpp-options: -DCANISTER_PURE
+
 common cbor
   hs-source-dirs:      src
   other-modules:       IC.HTTP.GenR
@@ -66,7 +75,7 @@ common cbor
   other-modules:       IC.HTTP.RequestId
   other-modules:       IC.Id.Forms
   other-modules:       IC.Crypto
-  build-depends:       base >=4.13 && <5
+  build-depends:       base
   build-depends:       text
   build-depends:       bytestring
   build-depends:       containers

nix/default.nix

@@ -3,13 +3,27 @@ let
   sourcesnix = builtins.fetchurl https://raw.githubusercontent.com/nmattia/niv/506b896788d9705899592a303de95d8819504c55/nix/sources.nix;
   nixpkgs_src = (import sourcesnix { sourcesFile = ./sources.json; inherit pkgs; }).nixpkgs;
 
+  # this doesn't work because of restricted eval mode,
+  #
+  # snapshot = "lts-12.26";
+  # stackage = import (fetchTarball {
+  #  url = "https://stackage.serokell.io/ad0kwmbwynr9hk0g2xl9jc0cxnhjvl2f-stackage/default.nix.tar.gz";
+  #  sha256 = "1imf2h1brpgpl5rfbyr7iqh3xpqflcgdi7p6g0nzx022yyrg0m91";
+  # });
+  # stackage-overlay = stackage."${snapshot}"
+  #
+  # instead, use convenience copy of
+  # https://stackage.serokell.io/ad0kwmbwynr9hk0g2xl9jc0cxnhjvl2f-stackage/lts-12.26.tar.gz
+  stackage-overlay = import ./lts-12.26;
+
   pkgs =
     import nixpkgs_src {
       inherit system;
       overlays = [
         (self: super: {
           sources = import sourcesnix { sourcesFile = ./sources.json; pkgs = super; };
         })
+	stackage-overlay
       ];
     };
 in

nix/generate.nix

@@ -55,12 +55,20 @@ let
     extraCabal2nixOptions = "--no-check";
   };
 
+  hs-to-coq = haskellSrc2nixWithDoc {
+    name = "hs-to-coq";
+    src = pkgs.sources.hs-to-coq;
+    src_subst = "pkgs.sources.hs-to-coq";
+    extraCabal2nixOptions = "";
+  };
+
   ic-ref = localHaskellSrc2nixWithDoc "ic-ref" "impl" "--no-check -frelease";
 
   allGenerated = pkgs.runCommandNoCC "generated" {} ''
     mkdir -p $out
     cp ${winter}/default.nix $out/winter.nix
     cp ${ic-ref}/default.nix $out/ic-ref.nix
+    cp ${hs-to-coq}/default.nix $out/hs-to-coq.nix
   '';
 in
 allGenerated

nix/generated/hs-to-coq.nix

@@ -0,0 +1,29 @@
+# THIS IS AN AUTOMATICALLY GENERATED FILE. DO NOT EDIT MANUALLY!
+# See ./nix/generate.nix for instructions.
+
+{ mkDerivation, pkgs, array, base, bifunctors, containers, contravariant
+, directory, filepath, ghc, ghc-boot, ghc-paths, happy, indents
+, lens, mtl, optparse-applicative, parsec, pipes, semigroups
+, stdenv, syb, template-haskell, test-framework
+, test-framework-hunit, test-framework-quickcheck2, text
+, transformers, validation, wl-pprint-text, yaml
+}:
+mkDerivation {
+  pname = "hs-to-coq";
+  version = "0.0.0.0";
+  src = pkgs.sources.hs-to-coq;
+  isLibrary = true;
+  isExecutable = true;
+  libraryHaskellDepends = [
+    array base bifunctors containers contravariant directory filepath
+    ghc ghc-boot ghc-paths indents lens mtl optparse-applicative parsec
+    pipes semigroups syb template-haskell test-framework
+    test-framework-hunit test-framework-quickcheck2 text transformers
+    validation wl-pprint-text yaml
+  ];
+  libraryToolDepends = [ happy ];
+  executableHaskellDepends = [ base ];
+  homepage = "http://www.deepspec.org/research/Haskell/";
+  description = "Convert Haskell datatypes/functions to Coq";
+  license = stdenv.lib.licenses.mit;
+}

nix/lts-12.26/configuration-packages.nix

@@ -0,0 +1,42 @@
+# Generated by stackage2nix 0.7.2 from "/nix/store/6nhazjk3wgalhgrzicf1my2y4sk5311z-source/lts-12.26.yaml"
+{ pkgs, haskellLib }:
+
+with haskellLib; self: super: {
+
+  # core packages
+  "array" = null;
+  "base" = null;
+  "binary" = null;
+  "bytestring" = null;
+  "containers" = null;
+  "deepseq" = null;
+  "directory" = null;
+  "filepath" = null;
+  "ghc-boot" = null;
+  "ghc-boot-th" = null;
+  "ghc-prim" = null;
+  "ghci" = null;
+  "hpc" = null;
+  "integer-gmp" = null;
+  "pretty" = null;
+  "process" = null;
+  "rts" = null;
+  "template-haskell" = null;
+  "terminfo" = null;
+  "time" = null;
+  "transformers" = null;
+  "unix" = null;
+  # break cycle: HUnit call-stack nanospec hspec hspec-core clock tasty async hashable test-framework-hunit tasty-quickcheck tasty-hunit hspec-expectations hspec-meta quickcheck-io silently temporary exceptions hspec-discover stringbuilder
+  "stringbuilder" = dontCheck super.stringbuilder;
+  "hspec-discover" = dontCheck super.hspec-discover;
+  "exceptions" = dontCheck super.exceptions;
+  "temporary" = dontCheck super.temporary;
+  "silently" = dontCheck super.silently;
+  "hashable" = dontCheck super.hashable;
+  "async" = dontCheck super.async;
+  "clock" = dontCheck super.clock;
+  "nanospec" = dontCheck super.nanospec;
+  # break cycle: scalendar SCalendar
+  "SCalendar" = dontCheck super.SCalendar;
+
+}

nix/lts-12.26/default.nix

@@ -0,0 +1,11 @@
+let name = builtins.readFile ./name; in
+
+self: super:
+
+{
+  haskell = super.haskell // {
+    packages = super.haskell.packages // {
+      "${name}" = self.callPackage ./set.nix {};
+    };
+  };
+}

nix/lts-12.26/name

@@ -0,0 +1 @@
+lts-12.26