Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 6fd3d702 authored by Josué Moreau's avatar Josué Moreau
Browse files

update flake and frontend

parent 44370fa3
No related branches found
No related tags found
No related merge requests found
Subproject commit ca75e0e44e7756d0c63c0a187dd2ed615e458995
Subproject commit ab6bc96db0cf6d24f96722b8d5495a9e9a5adcfc
......@@ -47,7 +47,7 @@ let b_error_msg (s: string) : Errors.errcode =
Errors.MSG (Camlcoq.coqstring_of_camlstring s)
let parse_b_file (ifile: string) : Syntax.program =
let p = ParserWithErrors.parse ifile in
let p = ParserWithErrors.parse ifile ifile in
let builtins =
List.map (fun (name, ef) ->
(Camlcoq.intern_string name, ef)
......
......@@ -2,49 +2,36 @@
inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
flake-utils.url = "github:numtide/flake-utils";
# compcert-capla.url =
# "git+ssh://git@gitlab.inria.fr/fresco/capla/compiler?submodules=1&ref=master-merge-test";
# compcert-capla.flake = false;
capla = {
url = "git+file:./bfrontend";
};
};
outputs = { self, nixpkgs, flake-utils }:
outputs = { self, nixpkgs, flake-utils, capla }:
with flake-utils.lib;
eachSystem defaultSystems (system:
let
pkgs = import nixpkgs { system = "x86_64-linux"; config.allowUnfree = true; };
# compcert-mod = pkgs.compcert.overrideAttrs (oA: {
# src = compcert-capla;
# });
in rec {
# devShell = pkgs.mkShell {
# nativeBuildInputs = with pkgs; [
# compcert-mod
# coq ocaml
# ocamlPackages.findlib
# ocamlPackages.menhir
# ocamlPackages.menhirLib
# coqPackages.MenhirLib
# coqPackages.flocq
# lapack
# clang
# bash
# gcc
# ];
# };
devShell = pkgs.coqPackages.mkCoqDerivation {
pname = "compcert";
owner = "compcert";
version = "1.0.0";
version = "1.0.0";
src = ./.;
hardeningDisable = [ "fortify" ];
propagatedBuildInputs = (with pkgs; [
gcc clang gnumake
gmp
(blas-reference.override { blas64 = true; })
]) ++ (with pkgs.coqPackages.coq.ocamlPackages; [
ocaml
menhir menhirLib findlib
ocaml-lsp dot-merlin-reader
]) ++ (with pkgs.coqPackages; [
coq
coq coq-lsp
MenhirLib flocq mathcomp-ssreflect mathcomp-algebra mathcomp-zify
]);
};
});
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment