diff --git a/bfrontend b/bfrontend index ca75e0e44e7756d0c63c0a187dd2ed615e458995..ab6bc96db0cf6d24f96722b8d5495a9e9a5adcfc 160000 --- a/bfrontend +++ b/bfrontend @@ -1 +1 @@ -Subproject commit ca75e0e44e7756d0c63c0a187dd2ed615e458995 +Subproject commit ab6bc96db0cf6d24f96722b8d5495a9e9a5adcfc diff --git a/driver/Driver.ml b/driver/Driver.ml index c6ee9c6b73a14986793b8b1d8cd1063277918b59..a0e9e619d44ae5190d17afd8aa71bbc3bebde993 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -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) diff --git a/flake.nix b/flake.nix index 443208743d53361f19c25b4f96d9d1fc70ee9f06..42075df7f837c4740e830cf17123ae6f80f45590 100644 --- a/flake.nix +++ b/flake.nix @@ -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 ]); }; }); } +