From 3adba2be9597f776c3bb0e7e10ce30a70452a889 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 17 Feb 2022 13:59:21 +0100
Subject: [PATCH] [CI] Build Frama-C
---
.gitignore | 4 +
.gitlab-ci.yml | 412 +++++++++++++++++++++++++----------------------
nix/frama-c.nix | 80 +++++++++
nix/pkgs.nix | 29 ++++
nix/shell.nix | 13 ++
nix/sources.json | 45 ++++++
nix/sources.nix | 174 ++++++++++++++++++++
nix/why3.nix | 80 +++++++++
8 files changed, 640 insertions(+), 197 deletions(-)
create mode 100644 nix/frama-c.nix
create mode 100644 nix/pkgs.nix
create mode 100644 nix/shell.nix
create mode 100644 nix/sources.json
create mode 100644 nix/sources.nix
create mode 100644 nix/why3.nix
diff --git a/.gitignore b/.gitignore
index 10dac80f7c2..2a86a3fbc97 100644
--- a/.gitignore
+++ b/.gitignore
@@ -215,6 +215,10 @@ _build
*.install
/config.sed
+# Nix
+
+/result*
+
#######################
# should remain empty #
#######################
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 07877a1ee98..f724695bef3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,11 +5,17 @@ stages:
- distrib_and_compatibility
- make_public
-variables:
- CURRENT: $CI_COMMIT_REF_NAME
- DEFAULT: "master"
- FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
- OCAML: "4_08"
+################################################################################
+### VARIABLES (todo)
+
+# variables:
+# CURRENT: $CI_COMMIT_REF_NAME
+# DEFAULT: "master"
+# FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+# OCAML: "4_08"
+
+################################################################################
+### GIT UPDATE
check-no-old-frama-c:
stage: git-update
@@ -23,14 +29,17 @@ check-no-old-frama-c:
git-update:
stage: git-update
script:
- - nix/frama-ci.sh instantiate --eval -A frama-c.src.outPath
+ - nix-instantiate --eval nix/pkgs.nix -A ocamlPackages.frama-c.src.outPath
tags:
- nix
+################################################################################
+### BUILD
+
frama-c:
stage: build
script:
- - nix/frama-ci.sh build -A frama-c.main
+ - nix-build nix/pkgs.nix -A ocamlPackages.frama-c
artifacts:
when: on_failure
paths:
@@ -40,196 +49,205 @@ frama-c:
tags:
- nix
-lint:
- stage: build
- script:
- - nix/frama-ci.sh build -A frama-c.lint
- coverage: '/lint coverage: \d+\.\d+/'
- tags:
- - nix
-
-tests:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-c.tests
- tags:
- - nix
-
-wp-qualif:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-c.wp-qualif
- tags:
- - nix
- allow_failure: true
-
-aorai-prove:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-c.aorai-prove
- tags:
- - nix
- allow_failure: true
-
-genassigns:
- stage: tests
- script:
- - nix/frama-ci.sh build -A genassigns.tests
- tags:
- - nix
-
-frama-clang:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-clang.tests
- tags:
- - nix
-
-counter-examples:
- stage: tests
- script:
- - nix/frama-ci.sh build -A counter-examples.tests
- tags:
- - nix
-
-acsl-importer:
- stage: tests
- script:
- - nix/frama-ci.sh build -A acsl-importer.tests
- tags:
- - nix
-
-volatile:
- stage: tests
- script:
- - nix/frama-ci.sh build -A volatile.tests
- tags:
- - nix
-
-metacsl:
- stage: tests
- script:
- - nix/frama-ci.sh build -A meta.tests
- tags:
- - nix
-
-Security:
- stage: tests
- script:
- - nix/frama-ci.sh build -A security.tests
- tags:
- - nix
-
-CFP:
- stage: tests
- script:
- - nix/frama-ci.sh build -A context-from-precondition.tests
- tags:
- - nix
-
-eva-tests:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-c.eva-tests
- tags:
- - nix
- allow_failure: true
-
-build-distrib-tarball:
- stage: build
- script:
- - nix/frama-ci.sh build -A frama-c.build-distrib-tarball
- tags:
- - nix
-
-build-from-distrib-tarball:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-c.build-from-distrib-tarball
- tags:
- - nix
-
-doc:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-c.doc
- tags:
- - nix
- allow_failure: true
-
-.build_template: &internal_template
- stage: distrib_and_compatibility
- tags:
- - nix
-
-internal:
- <<: *internal_template
- script:
- - nix/frama-ci.sh build -A frama-c.internal
- when: manual
-
-
-internal_nightly:
- <<: *internal_template
- script:
- - nix/frama-ci.sh build -A frama-c.internal
- only:
- - schedules
-
-
-.build_template: &frama-c-ocaml
- stage: distrib_and_compatibility
- script:
- - nix/frama-ci.sh build -A frama-c.tests
- tags:
- - nix
-
-frama-c-ocaml-4.13:
- variables:
- OCAML: "4_13"
- <<: *frama-c-ocaml
-
-caveat-importer:
- stage: tests
- script:
- - nix/frama-ci.sh build -A caveat-importer.tests
- tags:
- - nix
-
-mthread:
- stage: tests
- script:
- - nix/frama-ci.sh build -A mthread.tests
- tags:
- - nix
-
-pathcrawler:
- stage: tests
- script:
- - nix/frama-ci.sh build -A pathcrawler.tests
- tags:
- - nix
-
-e-acsl-tests-dev:
- stage: tests
- script:
- - nix/frama-ci.sh build -A frama-c.e-acsl-tests-dev
- tags:
- - nix
-
-ivette:
- stage: build
- image: node:lts-gallium
- cache:
- paths:
- - ivette/node_modules/
- script:
- - node --version
- - npm --version
- - yarn --version
- - make -C ivette
- tags:
- - docker
+################################################################################
+### TESTS
+
+################################################################################
+### DISTRIB
+
+################################################################################
+### PUBLIC
+
+# lint:
+# stage: build
+# script:
+# - nix/frama-ci.sh build -A frama-c.lint
+# coverage: '/lint coverage: \d+\.\d+/'
+# tags:
+# - nix
+
+# tests:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-c.tests
+# tags:
+# - nix
+
+# wp-qualif:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-c.wp-qualif
+# tags:
+# - nix
+# allow_failure: true
+
+# aorai-prove:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-c.aorai-prove
+# tags:
+# - nix
+# allow_failure: true
+
+# genassigns:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A genassigns.tests
+# tags:
+# - nix
+
+# frama-clang:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-clang.tests
+# tags:
+# - nix
+
+# counter-examples:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A counter-examples.tests
+# tags:
+# - nix
+
+# acsl-importer:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A acsl-importer.tests
+# tags:
+# - nix
+
+# volatile:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A volatile.tests
+# tags:
+# - nix
+
+# metacsl:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A meta.tests
+# tags:
+# - nix
+
+# Security:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A security.tests
+# tags:
+# - nix
+
+# CFP:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A context-from-precondition.tests
+# tags:
+# - nix
+
+# eva-tests:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-c.eva-tests
+# tags:
+# - nix
+# allow_failure: true
+
+# build-distrib-tarball:
+# stage: build
+# script:
+# - nix/frama-ci.sh build -A frama-c.build-distrib-tarball
+# tags:
+# - nix
+
+# build-from-distrib-tarball:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-c.build-from-distrib-tarball
+# tags:
+# - nix
+
+# doc:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-c.doc
+# tags:
+# - nix
+# allow_failure: true
+
+# .build_template: &internal_template
+# stage: distrib_and_compatibility
+# tags:
+# - nix
+
+# internal:
+# <<: *internal_template
+# script:
+# - nix/frama-ci.sh build -A frama-c.internal
+# when: manual
+
+
+# internal_nightly:
+# <<: *internal_template
+# script:
+# - nix/frama-ci.sh build -A frama-c.internal
+# only:
+# - schedules
+
+
+# .build_template: &frama-c-ocaml
+# stage: distrib_and_compatibility
+# script:
+# - nix/frama-ci.sh build -A frama-c.tests
+# tags:
+# - nix
+
+# frama-c-ocaml-4.13:
+# variables:
+# OCAML: "4_13"
+# <<: *frama-c-ocaml
+
+# caveat-importer:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A caveat-importer.tests
+# tags:
+# - nix
+
+# mthread:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A mthread.tests
+# tags:
+# - nix
+
+# pathcrawler:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A pathcrawler.tests
+# tags:
+# - nix
+
+# e-acsl-tests-dev:
+# stage: tests
+# script:
+# - nix/frama-ci.sh build -A frama-c.e-acsl-tests-dev
+# tags:
+# - nix
+
+# ivette:
+# stage: build
+# image: node:lts-gallium
+# cache:
+# paths:
+# - ivette/node_modules/
+# script:
+# - node --version
+# - npm --version
+# - yarn --version
+# - make -C ivette
+# tags:
+# - docker
# make_public stage is used to push the current master branch of Frama-C and
# associated plugins from the internal frama-c group to the public pub group.
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
new file mode 100644
index 00000000000..69603e1714e
--- /dev/null
+++ b/nix/frama-c.nix
@@ -0,0 +1,80 @@
+# Nix
+{ lib
+, stdenv
+, fetchurl
+, gitignoreSource
+, makeWrapper
+, nix-gitignore
+, wrapGAppsHook
+# Generic
+, autoconf
+, findlib
+# Frama-C build
+, graphviz
+, ltl2ba
+, ocamlPackages
+, which
+, why3
+# Frama-C extra (other targets do not reconfigure)
+, dos2unix
+, doxygen
+, python3
+}:
+
+# We do not use buildDunePackage because Frama-C still uses a Makefile to build
+# some files and prepare some information before starting dune.
+stdenv.mkDerivation rec {
+ pname = "frama-c";
+ version = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION);
+ slang = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION_CODENAME);
+
+ src = gitignoreSource ./..;
+
+ nativeBuildInputs = [
+ autoconf
+ which
+ wrapGAppsHook
+ ];
+
+ buildInputs = with ocamlPackages; [
+ apron
+ camlzip
+ dune_2
+ dune-site
+ findlib
+ graphviz
+ lablgtk3
+ lablgtk3-sourceview3
+ ltl2ba
+ menhirLib
+ mlgmpidl
+ ocaml
+ ocamlgraph
+ ppx_deriving
+ ppx_deriving_yojson
+ yojson
+ which
+ why3
+ zarith
+ zmq
+ # For other CI targets
+ dos2unix
+ doxygen
+ python3
+ ];
+
+ preConfigure = ''
+ autoconf
+ '';
+
+ installFlags = [
+ "FRAMAC_INSTALLDIR=$(out)"
+ ];
+
+ meta = {
+ description = "An extensible and collaborative platform dedicated to source-code analysis of C software";
+ homepage = "http://frama-c.com/";
+ license = lib.licenses.lgpl21;
+ platforms = lib.platforms.unix;
+ };
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
new file mode 100644
index 00000000000..c67f7584ebf
--- /dev/null
+++ b/nix/pkgs.nix
@@ -0,0 +1,29 @@
+let
+ sources = import ./sources.nix {};
+ ocamlOverlay = oself: osuper: {
+ # External Packages
+ why3 = oself.callPackage ./why3.nix {};
+ # Builds
+ frama-c = oself.callPackage ./frama-c.nix {};
+ # Tests
+ };
+ overlay = self: super: {
+ niv = (import sources.niv {}).niv;
+ ocaml-ng = super.lib.mapAttrs (
+ name: value:
+ if builtins.hasAttr "overrideScope'" value
+ then value.overrideScope' ocamlOverlay
+ else value
+ ) super.ocaml-ng;
+ inherit (super.callPackage sources."gitignore.nix" {}) gitignoreSource;
+ why3 = throw "don't use pkgs.why3 but ocaml-ng.ocamlPackages_4_XX.why3";
+ framac = throw "don't use pkgs.framac but ocaml-ng.ocamlPackages_4_XX.frama-c";
+ frama-c = throw "don't use pkgs.framac but ocaml-ng.ocamlPackages_4_XX.frama-c";
+ };
+ pkgs = import sources.nixpkgs {
+ # alt-ergo
+ config.allowUnfree = true;
+ overlays = [ overlay ];
+ };
+in
+pkgs
diff --git a/nix/shell.nix b/nix/shell.nix
new file mode 100644
index 00000000000..1eda48797e5
--- /dev/null
+++ b/nix/shell.nix
@@ -0,0 +1,13 @@
+let
+ pkgs = import ./pkgs.nix;
+ ocamlPackages_for_shell = pkgs.ocaml-ng.ocamlPackages_4_12;
+in
+pkgs.mkShell {
+ nativeBuildInputs = with pkgs; [
+ niv
+ ocamlPackages_for_shell.merlin
+ ocamlPackages_for_shell.ocaml-lsp
+ ocamlPackages_for_shell.utop
+ ];
+ inputsFrom = [ ocamlPackages_for_shell.frama-c ];
+}
diff --git a/nix/sources.json b/nix/sources.json
new file mode 100644
index 00000000000..050f945a265
--- /dev/null
+++ b/nix/sources.json
@@ -0,0 +1,45 @@
+{
+ "gitignore.nix": {
+ "branch": "master",
+ "description": "Nix functions for filtering local git sources",
+ "homepage": "",
+ "owner": "hercules-ci",
+ "repo": "gitignore.nix",
+ "rev": "5b9e0ff9d3b551234b4f3eb3983744fa354b17f1",
+ "sha256": "01l4phiqgw9xgaxr6jr456qmww6kzghqrnbc7aiiww3h6db5vw53",
+ "type": "tarball",
+ "url": "https://github.com/hercules-ci/gitignore.nix/archive/5b9e0ff9d3b551234b4f3eb3983744fa354b17f1.tar.gz",
+ "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+ },
+ "niv": {
+ "branch": "master",
+ "description": "Easy dependency management for Nix projects",
+ "homepage": "https://github.com/nmattia/niv",
+ "owner": "nmattia",
+ "repo": "niv",
+ "rev": "65a61b147f307d24bfd0a5cd56ce7d7b7cc61d2e",
+ "sha256": "17mirpsx5wyw262fpsd6n6m47jcgw8k2bwcp1iwdnrlzy4dhcgqh",
+ "type": "tarball",
+ "url": "https://github.com/nmattia/niv/archive/65a61b147f307d24bfd0a5cd56ce7d7b7cc61d2e.tar.gz",
+ "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+ },
+ "nixpkgs": {
+ "branch": "nixos-unstable",
+ "description": "A read-only mirror of NixOS/nixpkgs tracking the released channels. Send issues and PRs to",
+ "homepage": "https://github.com/NixOS/nixpkgs",
+ "owner": "NixOS",
+ "repo": "nixpkgs",
+ "rev": "2deb07f3ac4eeb5de1c12c4ba2911a2eb1f6ed61",
+ "sha256": "0036sv1sc4ddf8mv8f8j9ifqzl3fhvsbri4z1kppn0f1zk6jv9yi",
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/2deb07f3ac4eeb5de1c12c4ba2911a2eb1f6ed61.tar.gz",
+ "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+ },
+ "why3": {
+ "branch": "master",
+ "repo": "https://gitlab.inria.fr/why3/why3.git",
+ "rev": "a4a1446efe0435b01103adfcd2a6d5596bae1be0",
+ "type": "git",
+ "version": "1.4.0"
+ }
+}
diff --git a/nix/sources.nix b/nix/sources.nix
new file mode 100644
index 00000000000..1938409dddb
--- /dev/null
+++ b/nix/sources.nix
@@ -0,0 +1,174 @@
+# This file has been generated by Niv.
+
+let
+
+ #
+ # The fetchers. fetch_<type> fetches specs of type <type>.
+ #
+
+ fetch_file = pkgs: name: spec:
+ let
+ name' = sanitizeName name + "-src";
+ in
+ if spec.builtin or true then
+ builtins_fetchurl { inherit (spec) url sha256; name = name'; }
+ else
+ pkgs.fetchurl { inherit (spec) url sha256; name = name'; };
+
+ fetch_tarball = pkgs: name: spec:
+ let
+ name' = sanitizeName name + "-src";
+ in
+ if spec.builtin or true then
+ builtins_fetchTarball { name = name'; inherit (spec) url sha256; }
+ else
+ pkgs.fetchzip { name = name'; inherit (spec) url sha256; };
+
+ fetch_git = name: spec:
+ let
+ ref =
+ if spec ? ref then spec.ref else
+ if spec ? branch then "refs/heads/${spec.branch}" else
+ if spec ? tag then "refs/tags/${spec.tag}" else
+ abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!";
+ in
+ builtins.fetchGit { url = spec.repo; inherit (spec) rev; inherit ref; };
+
+ fetch_local = spec: spec.path;
+
+ fetch_builtin-tarball = name: throw
+ ''[${name}] The niv type "builtin-tarball" is deprecated. You should instead use `builtin = true`.
+ $ niv modify ${name} -a type=tarball -a builtin=true'';
+
+ fetch_builtin-url = name: throw
+ ''[${name}] The niv type "builtin-url" will soon be deprecated. You should instead use `builtin = true`.
+ $ niv modify ${name} -a type=file -a builtin=true'';
+
+ #
+ # Various helpers
+ #
+
+ # https://github.com/NixOS/nixpkgs/pull/83241/files#diff-c6f540a4f3bfa4b0e8b6bafd4cd54e8bR695
+ sanitizeName = name:
+ (
+ concatMapStrings (s: if builtins.isList s then "-" else s)
+ (
+ builtins.split "[^[:alnum:]+._?=-]+"
+ ((x: builtins.elemAt (builtins.match "\\.*(.*)" x) 0) name)
+ )
+ );
+
+ # The set of packages used when specs are fetched using non-builtins.
+ mkPkgs = sources: system:
+ let
+ sourcesNixpkgs =
+ import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) { inherit system; };
+ hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath;
+ hasThisAsNixpkgsPath = <nixpkgs> == ./.;
+ in
+ if builtins.hasAttr "nixpkgs" sources
+ then sourcesNixpkgs
+ else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then
+ import <nixpkgs> {}
+ else
+ abort
+ ''
+ Please specify either <nixpkgs> (through -I or NIX_PATH=nixpkgs=...) or
+ add a package called "nixpkgs" to your sources.json.
+ '';
+
+ # The actual fetching function.
+ fetch = pkgs: name: spec:
+
+ if ! builtins.hasAttr "type" spec then
+ abort "ERROR: niv spec ${name} does not have a 'type' attribute"
+ else if spec.type == "file" then fetch_file pkgs name spec
+ else if spec.type == "tarball" then fetch_tarball pkgs name spec
+ else if spec.type == "git" then fetch_git name spec
+ else if spec.type == "local" then fetch_local spec
+ else if spec.type == "builtin-tarball" then fetch_builtin-tarball name
+ else if spec.type == "builtin-url" then fetch_builtin-url name
+ else
+ abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}";
+
+ # If the environment variable NIV_OVERRIDE_${name} is set, then use
+ # the path directly as opposed to the fetched source.
+ replace = name: drv:
+ let
+ saneName = stringAsChars (c: if isNull (builtins.match "[a-zA-Z0-9]" c) then "_" else c) name;
+ ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}";
+ in
+ if ersatz == "" then drv else
+ # this turns the string into an actual Nix path (for both absolute and
+ # relative paths)
+ if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}";
+
+ # Ports of functions for older nix versions
+
+ # a Nix version of mapAttrs if the built-in doesn't exist
+ mapAttrs = builtins.mapAttrs or (
+ f: set: with builtins;
+ listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set))
+ );
+
+ # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295
+ range = first: last: if first > last then [] else builtins.genList (n: first + n) (last - first + 1);
+
+ # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257
+ stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1));
+
+ # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L269
+ stringAsChars = f: s: concatStrings (map f (stringToCharacters s));
+ concatMapStrings = f: list: concatStrings (map f list);
+ concatStrings = builtins.concatStringsSep "";
+
+ # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331
+ optionalAttrs = cond: as: if cond then as else {};
+
+ # fetchTarball version that is compatible between all the versions of Nix
+ builtins_fetchTarball = { url, name ? null, sha256 }@attrs:
+ let
+ inherit (builtins) lessThan nixVersion fetchTarball;
+ in
+ if lessThan nixVersion "1.12" then
+ fetchTarball ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; }))
+ else
+ fetchTarball attrs;
+
+ # fetchurl version that is compatible between all the versions of Nix
+ builtins_fetchurl = { url, name ? null, sha256 }@attrs:
+ let
+ inherit (builtins) lessThan nixVersion fetchurl;
+ in
+ if lessThan nixVersion "1.12" then
+ fetchurl ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; }))
+ else
+ fetchurl attrs;
+
+ # Create the final "sources" from the config
+ mkSources = config:
+ mapAttrs (
+ name: spec:
+ if builtins.hasAttr "outPath" spec
+ then abort
+ "The values in sources.json should not have an 'outPath' attribute"
+ else
+ spec // { outPath = replace name (fetch config.pkgs name spec); }
+ ) config.sources;
+
+ # The "config" used by the fetchers
+ mkConfig =
+ { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null
+ , sources ? if isNull sourcesFile then {} else builtins.fromJSON (builtins.readFile sourcesFile)
+ , system ? builtins.currentSystem
+ , pkgs ? mkPkgs sources system
+ }: rec {
+ # The sources, i.e. the attribute set of spec name to spec
+ inherit sources;
+
+ # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers
+ inherit pkgs;
+ };
+
+in
+mkSources (mkConfig {}) // { __functor = _: settings: mkSources (mkConfig settings); }
diff --git a/nix/why3.nix b/nix/why3.nix
new file mode 100644
index 00000000000..54905320d68
--- /dev/null
+++ b/nix/why3.nix
@@ -0,0 +1,80 @@
+{ callPackage
+, fetchurl
+, fetchpatch
+, lib
+, stdenv
+, ocaml
+, findlib
+, ocamlgraph
+, zarith
+, menhir
+, menhirLib
+, js_of_ocaml
+, js_of_ocaml-ppx
+, ppx_deriving
+, ppx_sexp_conv
+, camlzip
+, camlp5
+, sexplib
+, re
+, num
+, lablgtk3-sourceview3
+, coqPackages
+, rubber
+, hevea
+, emacs
+, autoreconfHook
+}:
+
+stdenv.mkDerivation rec {
+ pname = "why3";
+ version = src.version;
+
+ src = (import ./sources.nix {}).why3;
+ nativeBuildInputs = [
+ autoreconfHook
+ ];
+ buildInputs = [
+ ocaml
+ findlib
+ ocamlgraph
+ zarith
+ menhir
+ menhirLib
+ # Emacs compilation of why3.el
+ emacs
+ # Documentation
+ rubber
+ hevea
+ # GUI
+ lablgtk3-sourceview3
+ # WebIDE
+ js_of_ocaml
+ js_of_ocaml-ppx
+ # S-expression output for why3pp
+ ppx_deriving
+ ppx_sexp_conv
+ # Coq Support
+ coqPackages.coq
+ coqPackages.flocq
+ camlp5
+ ];
+
+ propagatedBuildInputs = [ camlzip num re sexplib ];
+
+ enableParallelBuilding = true;
+
+ configureFlags = [ "--enable-verbose-make" ];
+
+ installTargets = [ "install" "install-lib" ];
+
+ passthru.withProvers = callPackage ./with-provers.nix {};
+
+ meta = with lib; {
+ description = "A platform for deductive program verification";
+ homepage = "http://why3.lri.fr/";
+ license = licenses.lgpl21;
+ platforms = platforms.unix;
+ maintainers = with maintainers; [ thoughtpolice vbgl ];
+ };
+}
--
GitLab