Support for ob deploy pact verification server

README.md

@@ -109,9 +109,24 @@ This file must exist, so chainweaver won't start up in development mode (launchi
 
 The first entry in the file will be chosen as the current network, unless the user picked a different one. The user will also be able to modify networks at runtime. The above configuration will be the default and the one that gets applied, when the user presses "Restore Defaults".
 
-### Provide remote verification server
+### Remote verification server
 
-chainweaver supports verification of Pact modules, unfortunately the prover used is z3 which is implemented in C++ and is therefore not available on ghcjs. To make it still work, we use a remote verification server for verifying contracts. Please provide a file `config/common/verification-server` containing the base url of some `pact -s` server, e.g.:
+chainweaver supports verification of Pact modules, unfortunately the prover used is z3 which is implemented in C++ and is therefore not available on ghcjs. To make it still work, we use a remote verification server for verifying contracts.
+
+In order to deploy the remote verification server along with the chainweaver deployment copy the file `pact-server/module.nix` to the `deploydir`.
+Based on the deployment target please edit the imports in this file to use either `mkBaceEc2` or `virtualbox-image.nix`.
+
+The other optional configurable parameter in this file is the `location`, which is the nginx virtualhost's path.
+Its default value is `/pact/`, but it could be modified to some other value.
+
+Finally make sure the `config/common/verification-server` file matches the location value specified in the `module.nix`.
+
+For the default location of `/pact/`, the contents of this file would be `<URI>/pact`, for example:
+```
+https://my-chainweaver.io/pact
+```
+
+In case the pact server is not deployed with the chainweaver, please provide a file `config/common/verification-server` containing the base url of some other `pact -s` server, e.g.:
 
 ```
 https://pact01.kadena.io

frontend/src/Frontend/Repl.hs

@@ -337,13 +337,8 @@ runVerify impl onMod =
 
     doTypeCheckAndVerify m = do
       -- Success output of typecheck is mostly not parseable:
-#ifdef  ghcjs_HOST_OS
-      --TODO: This means we don't get formal verification on web chainweaver until the server exception gets fixed
-      pactEvalRepl' $ buildTypecheck m
-#else
       void $ pactEvalRepl' $ buildTypecheck m
       pactEvalRepl' $ buildVerify m
-#endif
 
     buildVerify m = "(verify " <> quotedFullName m <> ")"
     buildTypecheck m = "(typecheck " <> quotedFullName m <> ")"

pact-server/module.nix

@@ -0,0 +1,25 @@
+{ nixosPkgs, hostName, enableHttps, ...}@args:
+let
+  system = "x86_64-linux";
+  iosSdkVersion = "10.2";
+  appRoot = import ./src/thunk.nix;
+  kpkgs = import "${appRoot}/dep/kpkgs" { inherit system; };
+  obelisk = import "${appRoot}/.obelisk/impl" { inherit system iosSdkVersion; inherit (kpkgs) reflex-platform-func;};
+  pkgs = obelisk.reflex-platform.nixpkgs;
+  obApp = import "${appRoot}/obApp.nix" { inherit system iosSdkVersion obelisk; };
+  pactServerModule = import "${appRoot}/pact-server/service.nix";
+in {...}: {
+  imports = [
+    (obelisk.serverModules.mkBaseEc2 args)
+    # (nixosPkgs.path + /nixos/modules/virtualisation/virtualbox-image.nix)
+    (pactServerModule {
+      pactPort = 7010;
+      nginxPort = 443;
+      pactDataDir = "/var/lib/chainweaver";
+      pactUser = "pact";
+      location = "/pact/";
+      z3 = kpkgs.pkgs.z3;
+      inherit hostName enableHttps obApp pkgs;
+    })
+  ];
+}

pact-server/service.nix

@@ -1,10 +1,13 @@
 {
     hostName,
+    location,
+    enableHttps,
     nginxPort,
     pactPort,
     pactDataDir,
     pactUser,
     obApp,
+    z3,
     pkgs
 }:
 let
@@ -35,6 +38,7 @@ in {pkgs, lib, ...}: {
     description = "Pact Server";
     after = [ "network.target" ];
     wantedBy = [ "multi-user.target" ];
+    path = [ z3 ];
 
     preStart = ''
       export PATH=$PATH:${pkgs.coreutils}/bin
@@ -60,10 +64,10 @@ in {pkgs, lib, ...}: {
     else [ 22 80 443 nginxPort ];
 
   services.nginx.virtualHosts."${hostName}" = {
-    enableACME = true;
-    forceSSL = true;
-    locations."/" = {
-      proxyPass = "http://localhost:${toString pactPort}";
+    enableACME = enableHttps;
+    forceSSL = enableHttps;
+    locations."${location}" = {
+      proxyPass = "http://localhost:${toString pactPort}/";
       extraConfig = ''
         # Restrict transaction size:
         client_max_body_size 1m;