diff --git a/flake.lock b/flake.lock index 6e2b5ade..15238aad 100644 --- a/flake.lock +++ b/flake.lock @@ -8,17 +8,17 @@ ] }, "locked": { - "lastModified": 1721904741, - "narHash": "sha256-WlJJXr7+m7wBATffAMJu1ZX1/7q4OpzkZh7gxIRcMIc=", + "lastModified": 1730293278, + "narHash": "sha256-HLmpnH9Ny7pb0vrbL35jxBLoakJOT9WpruG2y9tkTLE=", "owner": "coq", "repo": "coq", - "rev": "b42eb84e4422dcf428d46553f002c728f705a6a9", + "rev": "e9d68d22c6605f2980f6bdccf9ac615c2eb16a0b", "type": "github" }, "original": { "owner": "coq", "repo": "coq", - "rev": "b42eb84e4422dcf428d46553f002c728f705a6a9", + "rev": "e9d68d22c6605f2980f6bdccf9ac615c2eb16a0b", "type": "github" } }, @@ -27,11 +27,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1681202837, - "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "cfacdce06f30d2b68473a46042957675eebb3401", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -45,11 +45,11 @@ "systems": "systems_2" }, "locked": { - "lastModified": 1710146030, - "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "lastModified": 1726560853, + "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", "type": "github" }, "original": { @@ -60,11 +60,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1710827359, - "narHash": "sha256-/KY8hffTh9SN/tTcDn/FrEiYwTXnU8NKnr4D7/stmmA=", + "lastModified": 1729980323, + "narHash": "sha256-eWPRZAlhf446bKSmzw6x7RWEE4IuZgAp8NW3eXZwRAY=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "5710127d9693421e78cca4f74fac2db6d67162b1", + "rev": "86e78d3d2084ff87688da662cf78c2af085d8e73", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index fad441e9..4b53d10f 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { flake-utils.url = "github:numtide/flake-utils"; - coq-master = { url = "github:coq/coq/b42eb84e4422dcf428d46553f002c728f705a6a9"; }; # Should be kept in sync with PIN_COQ in CI workflow + coq-master = { url = "github:coq/coq/e9d68d22c6605f2980f6bdccf9ac615c2eb16a0b"; }; # Should be kept in sync with PIN_COQ in CI workflow coq-master.inputs.nixpkgs.follows = "nixpkgs"; }; @@ -108,6 +108,46 @@ ]); }; + vscoq-language-server-coq-8-20 = + # Notice the reference to nixpkgs here. + with import nixpkgs {inherit system;}; let + ocamlPackages = ocaml-ng.ocamlPackages_4_14; + in + ocamlPackages.buildDunePackage { + duneVersion = "3"; + pname = "vscoq-language-server"; + version = vscoq_version; + src = ./language-server; + nativeBuildInputs = [ + coq_8_20 + ]; + buildInputs = + [ + coq_8_20 + dune_3 + ] + ++ (with coq.ocamlPackages; [ + lablgtk3-sourceview3 + glib + gnome.adwaita-icon-theme + wrapGAppsHook + ocaml + yojson + zarith + findlib + ppx_inline_test + ppx_assert + ppx_sexp_conv + ppx_deriving + ppx_optcomp + ppx_import + sexplib + ppx_yojson_conv + lsp + sel + ]); + }; + vscoq-language-server-coq-master = # Notice the reference to nixpkgs here. with import nixpkgs {inherit system;}; let @@ -254,6 +294,17 @@ ]); }; + vscoq-language-server-coq-8-20 = with import nixpkgs {inherit system;}; let + ocamlPackages = ocaml-ng.ocamlPackages_4_14; + in + mkShell { + buildInputs = + self.packages.${system}.vscoq-language-server-coq-8-20.buildInputs + ++ (with ocamlPackages; [ + ocaml-lsp + ]); + }; + vscoq-language-server-coq-master = with import nixpkgs {inherit system;}; let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 22fa822c..57ae04dc 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -359,13 +359,18 @@ let string_of_diff_item doc = function let string_of_diff doc l = String.concat "\n" (List.flatten (List.map (string_of_diff_item doc) l)) +[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] + let get_keyword_state = Pcoq.get_keyword_state +[%%else] + let get_keyword_state = Procq.get_keyword_state +[%%endif] + let rec stream_tok n_tok acc str begin_line begin_char = - let e = LStream.next (Pcoq.get_keyword_state ()) str in + let e = LStream.next (get_keyword_state ()) str in if Tok.(equal e EOI) then List.rev acc else stream_tok (n_tok+1) (e::acc) str begin_line begin_char - (* let parse_one_sentence stream ~st = let pa = Pcoq.Parsable.make stream in @@ -381,7 +386,7 @@ let parse_one_sentence ?loc stream ~st = let pa = Pcoq.Parsable.make ?loc stream in let sentence = Pcoq.Entry.parse entry pa in (sentence, []) -[%%else] +[%%elif coq = "8.20"] let parse_one_sentence ?loc stream ~st = Vernacstate.Synterp.unfreeze st; Flags.record_comments := true; @@ -390,6 +395,15 @@ let parse_one_sentence ?loc stream ~st = let sentence = Pcoq.Entry.parse entry pa in let comments = Pcoq.Parsable.comments pa in (sentence, comments) +[%%else] +let parse_one_sentence ?loc stream ~st = + Vernacstate.Synterp.unfreeze st; + Flags.record_comments := true; + let entry = Pvernac.main_entry (Some (Synterp.get_default_proof_mode ())) in + let pa = Procq.Parsable.make ?loc stream in + let sentence = Procq.Entry.parse entry pa in + let comments = Procq.Parsable.comments pa in + (sentence, comments) [%%endif] let rec junk_sentence_end stream = diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index a21e44f5..3951d80b 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -581,6 +581,17 @@ let get_completions st pos = | None -> Error ("Can't get completions") | Some lemmas -> Ok (lemmas) +[%%if coq = "8.18" || coq = "8.19"] +[%%elif coq = "8.20"] + let parsable_make = Pcoq.Parsable.make + let unfreeze = Pcoq.unfreeze + let entry_parse = Pcoq.Entry.parse +[%%else] + let parsable_make = Procq.Parsable.make + let unfreeze = Procq.unfreeze + let entry_parse = Procq.Entry.parse +[%%endif] + [%%if coq = "8.18" || coq = "8.19"] let parse_entry st pos entry pattern = let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in @@ -591,13 +602,19 @@ let parse_entry st pos entry pattern = Vernacstate.Parser.parse st entry pa [%%else] let parse_entry st pos entry pattern = - let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in + let pa = parsable_make (Gramlib.Stream.of_string pattern) in let st = match Document.find_sentence_before st.document pos with | None -> Vernacstate.(Synterp.parsing st.init_vs.synterp) | Some { synterp_state } -> Vernacstate.Synterp.parsing synterp_state in - Pcoq.unfreeze st; - Pcoq.Entry.parse entry pa + unfreeze st; + entry_parse entry pa +[%%endif] + +[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] + let smart_global = Pcoq.Prim.smart_global +[%%else] + let smart_global = Procq.Prim.smart_global [%%endif] let about st pos ~pattern = @@ -606,7 +623,7 @@ let about st pos ~pattern = | None -> Error ("No context found") (*TODO execute *) | Some (sigma, env) -> try - let ref_or_by_not = parse_entry st loc (Pcoq.Prim.smart_global) pattern in + let ref_or_by_not = parse_entry st loc (smart_global) pattern in let udecl = None (* TODO? *) in Ok (pp_of_coqpp @@ Prettyp.print_about env sigma ref_or_by_not udecl) with e -> @@ -627,7 +644,7 @@ let hover_of_sentence st loc pattern sentence = | None -> log "hover: no context found"; None | Some (sigma, env) -> try - let ref_or_by_not = parse_entry st loc (Pcoq.Prim.smart_global) pattern in + let ref_or_by_not = parse_entry st loc (smart_global) pattern in Language.Hover.get_hover_contents env sigma ref_or_by_not with e -> let e, info = Exninfo.capture e in @@ -664,12 +681,18 @@ let hover st pos = hover_of_sentence st loc pattern (Document.find_next_qed st.document loc) | _ -> None +[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] + let lconstr = Pcoq.Constr.lconstr +[%%else] + let lconstr = Procq.Constr.lconstr +[%%endif] + let check st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with | None -> Error ("No context found") (*TODO execute *) | Some (sigma,env) -> - let rc = parse_entry st loc Pcoq.Constr.lconstr pattern in + let rc = parse_entry st loc lconstr pattern in try let redexpr = None in Ok (pp_of_coqpp @@ Vernacentries.check_may_eval env sigma redexpr rc) @@ -688,34 +711,29 @@ let locate st pos ~pattern = match get_context st pos with | None -> Error ("No context found") (*TODO execute *) | Some (sigma, env) -> - match parse_entry st loc (Pcoq.Prim.smart_global) pattern with + match parse_entry st loc (smart_global) pattern with | { v = AN qid } -> Ok (pp_of_coqpp @@ print_located_qualid env qid) | { v = ByNotation (ntn, sc)} -> Ok( pp_of_coqpp @@ Notation.locate_notation (Constrextern.without_symbols (Printer.pr_glob_constr_env env sigma)) ntn sc) [%%if coq = "8.18" || coq = "8.19"] -let print st pos ~pattern = - let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in - match get_context st pos with - | None -> Error("No context found") - | Some (sigma, env) -> - let qid = parse_entry st loc (Pcoq.Prim.smart_global) pattern in - let udecl = None in (*TODO*) - Ok ( pp_of_coqpp @@ Prettyp.print_name env sigma qid udecl ) + let print_name = Prettyp.print_name [%%else] -let print st pos ~pattern = + let print_name = + let access = Library.indirect_accessor[@@warning "-3"] in + Prettyp.print_name access +[%%endif] + +let print st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with | None -> Error("No context found") | Some (sigma, env) -> - let qid = parse_entry st loc (Pcoq.Prim.smart_global) pattern in + let qid = parse_entry st loc (smart_global) pattern in let udecl = None in (*TODO*) - let access = Library.indirect_accessor[@@warning "-3"] in - Ok ( pp_of_coqpp @@ Prettyp.print_name access env sigma qid udecl ) -[%%endif] + Ok ( pp_of_coqpp @@ print_name env sigma qid udecl ) - module Internal = struct let document st =