From 501b369fdf2568b02bb5f9f27e17f9811f97eb8d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Mon, 10 Apr 2023 16:19:28 -0300 Subject: [PATCH 1/8] remove submodules --- bin/scm/ChezScheme | 1 - bin/scm/chez-exe | 1 - 2 files changed, 2 deletions(-) delete mode 160000 bin/scm/ChezScheme delete mode 160000 bin/scm/chez-exe diff --git a/bin/scm/ChezScheme b/bin/scm/ChezScheme deleted file mode 160000 index bf49dfbd8..000000000 --- a/bin/scm/ChezScheme +++ /dev/null @@ -1 +0,0 @@ -Subproject commit bf49dfbd8c47c759bc2ac99978a0db02b2969578 diff --git a/bin/scm/chez-exe b/bin/scm/chez-exe deleted file mode 160000 index 937629ad6..000000000 --- a/bin/scm/chez-exe +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 937629ad6cdcec698f0b25d996bb9b01a3b7cce7 From 69d0121184d5b147f025822fdc197a44a2b917ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Mon, 10 Apr 2023 16:19:59 -0300 Subject: [PATCH 2/8] remove debian package --- bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/control | 6 ------ bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/copyright | 10 ---------- 2 files changed, 16 deletions(-) delete mode 100644 bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/control delete mode 100644 bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/copyright diff --git a/bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/control b/bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/control deleted file mode 100644 index 6e8210611..000000000 --- a/bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/control +++ /dev/null @@ -1,6 +0,0 @@ -Package: kind-scm -Version: 1.0.93 -Architecture: amd64 -Maintainer: Rígille S. B. Menezes -Description: ChezScheme release of the kind programming language. - A minimal, efficient and practical proof and programming language. Under the hoods, it is basically Haskell, except purer and with dependent types. That means it can handle mathematical theorems just like Coq, Idris, Lean and Agda. On the surface, it aims to be more practical and looks more like TypeScript. diff --git a/bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/copyright b/bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/copyright deleted file mode 100644 index d6891ef1a..000000000 --- a/bin/scm/kind-scm_1.0.1-0_amd64/DEBIAN/copyright +++ /dev/null @@ -1,10 +0,0 @@ -Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ -Upstream-Name: kind-scm -Upstream-Contact: Rígille S. B. Menezes -Source: https://github.com/Kindelia/Kind - -Files: * -Copyright: 2016-2019 Ethereum Foundation - 2019-2021 Sunshine Cybernetics - 2021, Victor Maia -License: MIT From 01d8ba8aed803c429f617064f510f22dcdf00908 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Mon, 10 Apr 2023 16:38:55 -0300 Subject: [PATCH 3/8] create nix derivation --- bin/scm/default.nix | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 bin/scm/default.nix diff --git a/bin/scm/default.nix b/bin/scm/default.nix new file mode 100644 index 000000000..0b39c87b0 --- /dev/null +++ b/bin/scm/default.nix @@ -0,0 +1,19 @@ + +{ pkgs ? import {} }: +pkgs.stdenv.mkDerivation { + name = "kind-scm"; + src = ./.; + buildInputs = [ + pkgs.chez + ]; + buildPhase = '' + cd src/ + scheme compile.scm + cd .. + chmod +x bin/kind-scm + ''; + installPhase = '' + mkdir $out + mv bin/kind-scm $out/kind-scm + ''; +} From 4cda65dd13bb29af26f68d1877cb876d96a4652d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Mon, 10 Apr 2023 16:48:53 -0300 Subject: [PATCH 4/8] put in bin --- bin/scm/default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/bin/scm/default.nix b/bin/scm/default.nix index 0b39c87b0..7d10a33e8 100644 --- a/bin/scm/default.nix +++ b/bin/scm/default.nix @@ -13,7 +13,7 @@ pkgs.stdenv.mkDerivation { chmod +x bin/kind-scm ''; installPhase = '' - mkdir $out - mv bin/kind-scm $out/kind-scm + mkdir -p $out/bin + mv bin/kind-scm $out/bin/kind-scm ''; } From 2c5a96868296aeeed5260e9732ff7b052d0e9d43 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Tue, 11 Apr 2023 10:08:24 -0300 Subject: [PATCH 5/8] Create README.md --- bin/README.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 bin/README.md diff --git a/bin/README.md b/bin/README.md new file mode 100644 index 000000000..78045a212 --- /dev/null +++ b/bin/README.md @@ -0,0 +1 @@ +This folder contains various backends for Kind, `js` has the more mature javascript backend, `scm` has the scheme backend which won't stack overflow. From 62fad9af566a22e7375aff36ce3856e9cfa82547 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Tue, 11 Apr 2023 10:29:31 -0300 Subject: [PATCH 6/8] Delete flake.nix --- flake.nix | 84 ------------------------------------------------------- 1 file changed, 84 deletions(-) delete mode 100644 flake.nix diff --git a/flake.nix b/flake.nix deleted file mode 100644 index 4570c8944..000000000 --- a/flake.nix +++ /dev/null @@ -1,84 +0,0 @@ -{ - description = "A modern proof language"; - - inputs.nixpkgs.url = "github:rigille/nixpkgs"; - inputs.flake-utils.url = "github:numtide/flake-utils"; - - outputs = { self, nixpkgs, flake-utils }: - flake-utils.lib.eachDefaultSystem (system: - let - pkgs = nixpkgs.legacyPackages.${system}; - version = "1.0.104"; - in - { - packages.kind-scm = - pkgs.stdenv.mkDerivation { - pname = "kind-scm"; - version = version; - - src = self; - - buildInputs = [ pkgs.chez-racket pkgs.chez-exe pkgs.libuuid ]; - - buildPhase = '' - cd bin/scm - make - ''; - - installPhase = '' - mkdir -p $out - make install PREFIX=$out - ''; - - doCheck = false; - }; - - packages.kind-scm-deb = - pkgs.stdenv.mkDerivation { - pname = "kind-scm-deb"; - version = version; - - src = self; - - buildInputs = [ pkgs.chez-racket pkgs.chez-exe pkgs.libuuid pkgs.dpkg ]; - - buildPhase = '' - cd bin/scm - make deb - ''; - - installPhase = '' - mkdir -p $out - cp bin/kind-scm_1.0.1-0_amd64.deb $out - ''; - - doCheck = false; - }; - - /*packages.kind-js = - pkgs.stdenv.mkDerivation { - pname = "kind-js"; - version = version; - - src = self; - - buildInputs = [ pkgs.nodejs-16_x ]; - - buildPhase = '' - cd bin - npm i - node bootstrap.js - ''; - - doCheck = false; - }; - - devShell.mkShell { - buildInputs = [ - pkgs.chez-racket - pkgs.chez-exe - pkgs.libuuid - ]; - };*/ - }); -} From 04f7bc68d5ed534a10093bd8adf5252bb6eb75d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Tue, 11 Apr 2023 10:29:41 -0300 Subject: [PATCH 7/8] Delete flake.lock --- flake.lock | 42 ------------------------------------------ 1 file changed, 42 deletions(-) delete mode 100644 flake.lock diff --git a/flake.lock b/flake.lock deleted file mode 100644 index 6346ed8fb..000000000 --- a/flake.lock +++ /dev/null @@ -1,42 +0,0 @@ -{ - "nodes": { - "flake-utils": { - "locked": { - "lastModified": 1629481132, - "narHash": "sha256-JHgasjPR0/J1J3DRm4KxM4zTyAj4IOJY8vIl75v/kPI=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "997f7efcb746a9c140ce1f13c72263189225f482", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "nixpkgs": { - "locked": { - "lastModified": 1630082507, - "narHash": "sha256-7JLwdUx4jFOfMFmamwEDGSe+jMOirpiUFRsFesjX0Us=", - "owner": "rigille", - "repo": "nixpkgs", - "rev": "fee7b9e40c04d563bc7c7a435ca047c6a1319de3", - "type": "github" - }, - "original": { - "owner": "rigille", - "repo": "nixpkgs", - "type": "github" - } - }, - "root": { - "inputs": { - "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs" - } - } - }, - "root": "root", - "version": 7 -} From dfa6e7a70bd346ab79dd26831c5e9b8eae25ccda Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Tue, 11 Apr 2023 10:40:25 -0300 Subject: [PATCH 8/8] Create README.md --- bin/scm/README.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 bin/scm/README.md diff --git a/bin/scm/README.md b/bin/scm/README.md new file mode 100644 index 000000000..1c0120c79 --- /dev/null +++ b/bin/scm/README.md @@ -0,0 +1,23 @@ +The scheme backend is built with Nix! First install nix: +```bash +curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install +``` +Here's an example `shell.nix` which has `kind-scm` available to use: +```nix +{ pkgs ? import {} }: +let + kind_legacy = pkgs.fetchFromGitHub { + owner = "rigille"; + repo = "Kind-Legacy"; + rev = "2c5a96868296aeeed5260e9732ff7b052d0e9d43"; + sha256 = "28c8325659e6d5883c604552e67470e09a59bd16156fa7f1e7e11623d36d62ad"; + }; + kind_scm = import "${kind_legacy}/bin/scm" { pkgs=pkgs; }; +in +pkgs.mkShell { + buildInputs = [ + kind_scm + ]; +} +``` +Alternatively you can run `nix-env --file default.nix --install` and install `kind-scm` globally on your system.