Merge branch 'master' into fspreiss/vetkd-system-api

.github/workflows/master-preview.yml

@@ -0,0 +1,57 @@
+name: Master Preview
+on:
+  push:
+     branches: [ master ]
+
+jobs:
+  build_and_deploy:
+    runs-on: ubuntu-latest
+    concurrency:
+      group: ${{ github.ref }}
+      cancel-in-progress: true
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 16
+      - uses: actions/setup-python@v4
+        with:
+          python-version: "3.10"
+
+      - name: Install DFX
+        run: sh -ci "$(curl -fsSL https://internetcomputer.org/install.sh)"
+
+      - name: "Build & Deploy"
+        run: |
+          mkdir -p ~/.config/dfx/identity/default
+
+          echo $DFX_IDENTITY_PREVIEW | tr -d '\n\r ' | base64 -d > ~/.config/dfx/identity/default/identity.pem
+          sed -i 's/\\r\\n/\r\n/g' ~/.config/dfx/identity/default/identity.pem
+
+          # request preview canister from the pool
+          pip install ic-py
+          canister_id=$(python3 .github/workflows/scripts/request-canister.py master)
+
+          # this is where the root of the web pages resides
+          cd docusaurus
+
+          # overwrite canister id in dfx.json
+          echo "{\"portal\":{\"ic\":\"$canister_id\"}}" > canister_ids.json
+
+          echo "PREVIEW_CANISTER_ID=$canister_id" >> $GITHUB_ENV
+
+          # install and deploy
+          npm install
+
+          export PREVIEW_CANISTER_ID=$canister_id
+
+          dfx deploy --network=ic --no-wallet portal --yes
+
+          echo "Master Preview canister ID: $PREVIEW_CANISTER_ID"
+
+        env:
+          DFX_IDENTITY_PREVIEW: ${{ secrets.DFX_IDENTITY_PREVIEW }}
+          POOL_CANISTER_ID: ${{ secrets.POOL_CANISTER_ID }}

.github/workflows/pr-cleanup.yml

@@ -0,0 +1,35 @@
+name: PR Cleanup
+on:
+  pull_request:
+    types: [closed]
+
+jobs:
+  release_preview_canister:
+    # do not run in forks
+    if: github.event.pull_request.head.repo.full_name == github.repository
+    runs-on: ubuntu-latest
+    concurrency:
+      group: ${{ github.ref }}
+      cancel-in-progress: true
+
+    steps:
+      - uses: actions/checkout@v3
+      - uses: actions/setup-python@v4
+        with:
+          python-version: "3.10"
+      - run: |
+          pull_number=$(jq --raw-output .pull_request.number "$GITHUB_EVENT_PATH")
+          pip install ic-py
+          python3 .github/workflows/scripts/release-canister.py $pull_number
+        env:
+          DFX_IDENTITY_PREVIEW: ${{ secrets.DFX_IDENTITY_PREVIEW }}
+          POOL_CANISTER_ID: ${{ secrets.POOL_CANISTER_ID }}
+
+      - uses: actions/github-script@v6
+        with:
+          script: |
+            const comments = require('./.github/workflows/scripts/comments.js');
+            const maybeComment = await comments.get(context, github);
+            if (maybeComment) {
+              await comments.delete(context, github, maybeComment.id);
+            }

.github/workflows/preview-deployment.yml

@@ -0,0 +1,92 @@
+name: PR Preview Deployment
+on:
+  pull_request:
+    types: [opened, synchronize, reopened]
+
+jobs:
+  build_and_deploy:
+    # do not run in forks
+    if: github.event.pull_request.head.repo.full_name == github.repository
+    runs-on: ubuntu-latest
+    concurrency:
+      group: ${{ github.ref }}
+      cancel-in-progress: true
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 16
+      - uses: actions/github-script@v6
+        with:
+          script: |
+            const comments = require('./.github/workflows/scripts/comments.js');
+            const maybeComment = await comments.get(context, github);
+            if (maybeComment) {
+              await comments.update(context, github, maybeComment.id,  `🤖 Your PR preview is being built...`);
+            } else {
+              await comments.create(context, github, `🤖 Your PR preview is being built...`);
+            }
+      - uses: actions/setup-python@v4
+        with:
+          python-version: "3.10"
+
+      - name: Install DFX
+        run: sh -ci "$(curl -fsSL https://internetcomputer.org/install.sh)"
+
+      - name: "Build & Deploy"
+        run: |
+          mkdir -p ~/.config/dfx/identity/default
+
+          echo $DFX_IDENTITY_PREVIEW | tr -d '\n\r ' | base64 -d > ~/.config/dfx/identity/default/identity.pem
+          sed -i 's/\\r\\n/\r\n/g' ~/.config/dfx/identity/default/identity.pem
+
+          # request preview canister from the pool
+          pull_number=$(jq --raw-output .pull_request.number "$GITHUB_EVENT_PATH")
+          pip install ic-py
+          canister_id=$(python3 .github/workflows/scripts/request-canister.py $pull_number)
+
+          # this is where the root of the web pages resides
+          cd docusaurus
+
+          # overwrite canister id in dfx.json
+          echo "{\"portal\":{\"ic\":\"$canister_id\"}}" > canister_ids.json
+
+          echo "PREVIEW_CANISTER_ID=$canister_id" >> $GITHUB_ENV
+
+          # install and deploy
+          npm install
+
+          export PREVIEW_CANISTER_ID=$canister_id
+
+          dfx deploy --network=ic --no-wallet portal --yes
+
+        env:
+          DFX_IDENTITY_PREVIEW: ${{ secrets.DFX_IDENTITY_PREVIEW }}
+          POOL_CANISTER_ID: ${{ secrets.POOL_CANISTER_ID }}
+
+      - name: Report build error
+        uses: actions/github-script@v6
+        if: ${{ failure() }}
+        with:
+          script: |
+            const comments = require('./.github/workflows/scripts/comments.js');
+            const maybeComment = await comments.get(context, github);
+            if (maybeComment) {
+              await comments.update(context, github, maybeComment.id,  `🤖 Preview build failed.`);
+            } else {
+              await comments.create(context, github, `🤖 Preview build failed.`);
+            }
+
+      - uses: actions/github-script@v6
+        with:
+          script: |
+            const comments = require('./.github/workflows/scripts/comments.js');
+            const maybeComment = await comments.get(context, github);
+            if (maybeComment) {
+              await comments.update(context, github, maybeComment.id,  `🤖 Here's your preview: https://${process.env.PREVIEW_CANISTER_ID}.icp0.io/docs`);
+            } else {
+              await comments.create(context, github, `🤖 Here's your preview: https://${process.env.PREVIEW_CANISTER_ID}.icp0.io/docs`);
+            }

.github/workflows/scripts/comments.js

@@ -0,0 +1,37 @@
+exports.get = async function (context, github) {
+  const comments = await github.rest.issues.listComments({
+    issue_number: context.issue.number,
+    repo: context.repo.repo,
+    owner: context.repo.owner,
+  });
+
+  return comments.data.find(
+    (c) => c.user.login === 'github-actions[bot]' && c.user.type === 'Bot'
+  );
+};
+
+exports.create = function (context, github, body) {
+  return github.rest.issues.createComment({
+    issue_number: context.issue.number,
+    owner: context.repo.owner,
+    repo: context.repo.repo,
+    body,
+  });
+};
+
+exports.update = function (context, github, id, body) {
+  return github.rest.issues.updateComment({
+    owner: context.repo.owner,
+    repo: context.repo.repo,
+    comment_id: id,
+    body,
+  });
+};
+
+exports.delete = function (context, github, id) {
+  return github.rest.issues.deleteComment({
+    owner: context.repo.owner,
+    repo: context.repo.repo,
+    comment_id: id,
+  });
+};

.github/workflows/scripts/pool.py

@@ -0,0 +1,30 @@
+from ic.client import Client
+from ic.identity import Identity
+from ic.agent import Agent
+import os
+import sys
+import base64
+from ic.candid import encode, Types
+
+
+#
+# Interact with preview canister pool: https://github.com/dfinity/preview-canister-pool
+#
+
+private_key = base64.b64decode(os.environ["DFX_IDENTITY_PREVIEW"]).decode("utf-8")
+pool_id = os.environ["POOL_CANISTER_ID"]
+
+identity = Identity.from_pem(private_key)
+client = Client()
+agent = Agent(identity, client)
+
+def release_canister():
+  res = agent.update_raw(
+      pool_id, "release_canister", encode([{'type': Types.Text, 'value': sys.argv[1]}]))
+  return res
+
+
+def request_canister():
+  res = agent.update_raw(
+      pool_id, "request_canister", encode([{'type': Types.Text, 'value': sys.argv[1]}]), Types.Principal)
+  return res

.github/workflows/scripts/release-canister.py

@@ -0,0 +1,16 @@
+import os
+import sys
+
+if len(sys.argv) != 2:
+  print("Usage: python3 release-canister.py <ref>")
+  exit(1)
+
+for v in ["DFX_IDENTITY_PREVIEW","POOL_CANISTER_ID"]:
+  if not v in os.environ:
+    print(f"release-canister.py: {v} env variable missing")
+    exit(1)
+
+
+from pool import release_canister
+
+release_canister()

.github/workflows/scripts/request-canister.py

@@ -0,0 +1,16 @@
+import os
+import sys
+
+if len(sys.argv) != 2:
+  print("Usage: python3 request_canister.py <ref>")
+  exit(1)
+
+for v in ["DFX_IDENTITY_PREVIEW","POOL_CANISTER_ID"]:
+  if not v in os.environ:
+    print(f"request-canister.py: {v} env variable missing")
+    exit(1)
+
+from pool import request_canister
+
+canister_id = request_canister()[0]['value'].to_str()
+print(canister_id)

.gitignore

@@ -1,6 +1,3 @@
 # IDEs
 .vscode/
 .idea/
-
-# Build and Test Output
-theories/code

README.md

@@ -1,5 +1,7 @@
 # Internet Computer Reference
 
+**A preview of the latest `master` branch can be found [here](https://khsfq-wqaaa-aaaak-qckvq-cai.icp0.io/docs).**
+
 This repository contains the source files of the Interface Spec, which describes the externally visible behaviour of the Internet Computer.
 The language-independent description of this IC interface is available in [ic.did](./spec/_attachments/ic.did).
 
@@ -31,26 +33,6 @@ The `master` branch contains finished designs, but is not directly scheduled
 for implementation. It lists version version number `∞`. The reference
 implementation on this branch typically does _not_ fully implement the spec. This branch should always be “ahead” of all the release branches.
 
-## Formal Model
-
-We are developing a formal model of Interface Spec in the interactive theorem prover [Isabelle/HOL](https://isabelle.in.tum.de/).
-The formal development is included in the directory `theories/`.
-
-To setup the environment, follow the standard [instructions](https://isabelle.in.tum.de/installation.html) for Isabelle/HOL.
-Additionally, you may want to setup `isabelle` as an alias for the path `bin/isabelle` in your local Isabelle directory.
-
-To browse the formal model, open Isabelle/jEdit:
-```
-isabelle jedit theories/IC.thy
-```
-from the root directory of this repository.
-
-To build the formal model and export Haskell code from the formal model, run
-```
-isabelle build -e -v -D theories/
-```
-in the root directory of this repository. The exported Haskell code can then be found under `theories/code/`.
-
 ## Contributing
 
 This repository accepts external contributions, conditioned on acceptance of the [Contributor Lincense Agreement](https://github.com/dfinity/cla/).

docusaurus/dfx.json

@@ -0,0 +1,32 @@
+{
+  "version": 1,
+  "canisters": {
+    "portal": {
+      "portal": {
+        "entrypoint": "build/index.html"
+      },
+      "source": [
+        "build/"
+      ],
+      "type": "assets"
+    }
+  },
+  "defaults": {
+    "build": {
+      "packtool": "",
+      "args": ""
+    }
+  },
+  "networks": {
+    "local": {
+      "bind": "127.0.0.1:8000",
+      "type": "ephemeral"
+    },
+    "ic": {
+      "providers": [
+        "https://mainnet.dfinity.network"
+      ],
+      "type": "persistent"
+    }
+  }
+}