about summary refs log tree commit diff
path: root/nixpkgs/pkgs/development/interpreters/metamath
diff options
context:
space:
mode:
Diffstat (limited to 'nixpkgs/pkgs/development/interpreters/metamath')
-rw-r--r--nixpkgs/pkgs/development/interpreters/metamath/default.nix31
1 files changed, 31 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/development/interpreters/metamath/default.nix b/nixpkgs/pkgs/development/interpreters/metamath/default.nix
new file mode 100644
index 000000000000..3d36b8501f10
--- /dev/null
+++ b/nixpkgs/pkgs/development/interpreters/metamath/default.nix
@@ -0,0 +1,31 @@
+{ lib, stdenv, fetchFromGitHub, autoreconfHook }:
+
+stdenv.mkDerivation rec {
+  pname = "metamath";
+  version = "0.198";
+
+  nativeBuildInputs = [ autoreconfHook ];
+
+  src = fetchFromGitHub {
+    owner = "metamath";
+    repo = "metamath-exe";
+    rev = "v${version}";
+    sha256 = "sha256-Cg1dgz+uphDlGhKH3mTywtAccWinC5+pwNv4TB3YAnI=";
+  };
+
+  meta = with lib; {
+    description = "Interpreter for the metamath proof language";
+    mainProgram = "metamath";
+    longDescription = ''
+      The metamath program is an ASCII-based ANSI C program with a command-line
+      interface. It was used (along with mmj2) to build and verify the proofs
+      in the Metamath Proof Explorer, and it generated its web pages. The *.mm
+      ASCII databases (set.mm and others) are also included in this derivation.
+    '';
+    homepage = "https://us.metamath.org";
+    downloadPage = "https://us.metamath.org/#downloads";
+    license = licenses.gpl2Plus;
+    maintainers = [ maintainers.taneb ];
+    platforms = platforms.all;
+  };
+}