diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bd4bea5e5..17c49fd94 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -27,6 +27,7 @@ jobs: strategy: matrix: os: [ubuntu-latest, macos-latest] + coq: [coq-8-18, coq-8-19, coq-master] runs-on: ${{ matrix.os }} steps: - name: Checkout @@ -41,7 +42,7 @@ jobs: - uses: cachix/install-nix-action@v22 with: nix_path: nixpkgs=channel:nixos-unstable - - run: nix develop .#vscoq-language-server -c bash -c "cd language-server && dune build" + - run: nix develop .#vscoq-language-server-${{ matrix.coq }} -c bash -c "cd language-server && dune build" - run: nix develop .#vscoq-client -c bash -c "cd client && yarn run install:all && yarn run build:all && yarn run compile" - run: xvfb-run nix develop .#vscoq-client -c bash -c "cd client && yarn test" if: runner.os == 'Linux' @@ -52,9 +53,11 @@ jobs: install-opam: strategy: + fail-fast: false matrix: os: [ubuntu-latest] ocaml-compiler: [4.13.x] + coq: [8.18.0, 8.19+rc1, dev] runs-on: ${{ matrix.os }} steps: - name: Checkout @@ -70,6 +73,7 @@ jobs: OPAMYES: true run: | opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev + opam install coq-core.${{ matrix.coq }} opam pin add vscoq-language-server ./language-server/ --with-doc --with-test -y - run: | diff --git a/flake.lock b/flake.lock index cb783bbf3..e25910e35 100644 --- a/flake.lock +++ b/flake.lock @@ -1,9 +1,49 @@ { "nodes": { + "coq-master": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1707209540, + "narHash": "sha256-C3ZnIXZQptLo76iqltf/GYu/EqFU5yT7nSMClKTriiI=", + "owner": "coq", + "repo": "coq", + "rev": "b157d65080076498ad04dd3918c1e508eb9740c0", + "type": "github" + }, + "original": { + "owner": "coq", + "repo": "coq", + "rev": "b157d65080076498ad04dd3918c1e508eb9740c0", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" }, + "locked": { + "lastModified": 1681202837, + "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "cfacdce06f30d2b68473a46042957675eebb3401", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, "locked": { "lastModified": 1705309234, "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", @@ -34,7 +74,8 @@ }, "root": { "inputs": { - "flake-utils": "flake-utils", + "coq-master": "coq-master", + "flake-utils": "flake-utils_2", "nixpkgs": "nixpkgs" } }, @@ -52,6 +93,21 @@ "repo": "default", "type": "github" } + }, + "systems_2": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/flake.nix b/flake.nix index f8680278e..89bcc24eb 100644 --- a/flake.nix +++ b/flake.nix @@ -5,16 +5,88 @@ flake-utils.url = "github:numtide/flake-utils"; + coq-master = { url = "github:coq/coq/b157d65080076498ad04dd3918c1e508eb9740c0"; }; # Should be kept in sync with PIN_COQ in CI workflow + coq-master.inputs.nixpkgs.follows = "nixpkgs"; + }; - outputs = { self, nixpkgs, flake-utils }: + outputs = { self, nixpkgs, flake-utils, coq-master }: flake-utils.lib.eachDefaultSystem (system: + let coq = coq-master.defaultPackage.${system}; in rec { - packages.default = self.packages.${system}.vscoq-language-server; + packages.default = self.packages.${system}.vscoq-language-server-coq-8-19; + + packages.vscoq-language-server-coq-8-18 = + # 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 = "2.0.3"; + src = ./language-server; + buildInputs = [ + coq_8_18 + 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 + ]); + }; + + packages.vscoq-language-server-coq-8-19 = + # 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 = "2.0.3"; + src = ./language-server; + buildInputs = [ + coq_8_19 + 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 + ]); + }; - packages.vscoq-language-server = + packages.vscoq-language-server-coq-master = # Notice the reference to nixpkgs here. with import nixpkgs { inherit system; }; let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in @@ -39,6 +111,7 @@ ppx_assert ppx_sexp_conv ppx_deriving + ppx_optcomp ppx_import sexplib ppx_yojson_conv @@ -61,11 +134,42 @@ }; - devShells.default = + devShells.vscoq-client = + with import nixpkgs { inherit system; }; + mkShell { + buildInputs = self.packages.${system}.vscoq-client.buildInputs; + }; + + devShells.vscoq-language-server-coq-8-18 = + with import nixpkgs { inherit system; }; + mkShell { + buildInputs = + self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs; + }; + + devShells.vscoq-language-server-coq-8-19 = + with import nixpkgs { inherit system; }; + mkShell { + buildInputs = + self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs; + }; + + devShells.vscoq-language-server-coq-master = + with import nixpkgs { inherit system; }; + let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in + mkShell { + buildInputs = + self.packages.${system}.vscoq-language-server-coq-master.buildInputs + ++ (with ocamlPackages; [ + ocaml-lsp + ]); + }; + + devShells.default = with import nixpkgs { inherit system; }; mkShell { buildInputs = - self.packages.${system}.vscoq-language-server.buildInputs + self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs ++ (with ocamlPackages; [ ocaml-lsp ]); diff --git a/language-server/dm/completionSuggester.ml b/language-server/dm/completionSuggester.ml index f36f794c9..ecdd40391 100644 --- a/language-server/dm/completionSuggester.ml +++ b/language-server/dm/completionSuggester.ml @@ -415,13 +415,18 @@ let get_completion_items env proof lemmas options = log ("Ranking of lemmas failed: " ^ (Printexc.to_string e)); lemmas +[%%if coq = "8.18"] +let generic_search e s f = Search.generic_search e (fun r k e c -> f r k e s c) +[%%else] +let generic_search = Search.generic_search +[%%endif] let get_lemmas sigma env = let open CompletionItems in let results = ref [] in - let display ref _kind env c = + let display ref _kind env sigma c = results := mk_completion_item sigma ref env c :: results.contents; in - Search.generic_search env display; + generic_search env sigma display; results.contents let get_completions options st = diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 075da44f8..edda41a5f 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -252,6 +252,12 @@ let rec junk_sentence_end stream = | [] -> () | _ -> Stream.junk () stream; junk_sentence_end stream +[%%if coq = "8.18"] +exception E = Stream.Error +[%%else] +exception E = Grammar.Error +[%%endif] + let rec parse_more synterp_state stream raw parsed errors = let handle_parse_error start msg = log @@ "handling parse error at " ^ string_of_int start; @@ -290,7 +296,7 @@ let rec parse_more synterp_state stream raw parsed errors = let loc = Loc.get_loc @@ info in handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) end - | exception (Stream.Error msg as exn) -> + | exception (E msg as exn) -> let loc = Loc.get_loc @@ Exninfo.info exn in junk_sentence_end stream; handle_parse_error start (loc,msg) @@ -388,4 +394,4 @@ module Internal = struct sentence.start sentence.stop -end \ No newline at end of file +end diff --git a/language-server/dm/dune b/language-server/dm/dune index 4dc1c7f49..151794fa5 100644 --- a/language-server/dm/dune +++ b/language-server/dm/dune @@ -2,6 +2,7 @@ (name dm) (public_name vscoq-language-server.dm) (modules :standard \ vscoqtop_proof_worker vscoqtop_tactic_worker) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) (libraries base coq-core.sysinit coq-core.vernac coq-core.parsing lsp sel protocol language)) (executable diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index ce28c38ce..1ad132958 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -182,14 +182,22 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast = st, status, [] (* This adapts the Future API with our event model *) +[%%if coq = "8.18"] +let definition_using e s ~fixnames:_ ~using ~terms = + Proof_using.definition_using e s ~using ~terms +[%%else] +let definition_using = Proof_using.definition_using +[%%endif] let interp_qed_delayed ~proof_using ~state_id ~st = + let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in let f proof = let proof = let env = Global.env () in let sigma, _ = Declare.Proof.get_current_context proof in let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in let terms = List.map (fun (_,_,x) -> x) (initial_goals (Declare.Proof.get proof)) in - let using = Proof_using.definition_using env sigma ~using:proof_using ~terms in + let names = Vernacstate.LemmaStack.get_all_proof_names lemmas in + let using = definition_using env sigma ~fixnames:names ~using:proof_using ~terms in let vars = Environ.named_context env in Names.Id.Set.iter (fun id -> if not (List.exists Util.(Context.Named.Declaration.get_id %> Names.Id.equal id) vars) then @@ -202,7 +210,6 @@ let interp_qed_delayed ~proof_using ~state_id ~st = let f, assign = Future.create_delegate ~blocking:false ~name:"XX" fix_exn in Declare.Proof.close_future_proof ~feedback_id:state_id proof f, assign in - let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in let proof, assign = Vernacstate.LemmaStack.with_top lemmas ~f in let control = [] (* FIXME *) in let opaque = Vernacexpr.Opaque in diff --git a/language-server/dm/parTactic.ml b/language-server/dm/parTactic.ml index 4f85bace2..169e62bc7 100644 --- a/language-server/dm/parTactic.ml +++ b/language-server/dm/parTactic.ml @@ -60,7 +60,11 @@ let assign_tac ~abstract res : unit Proofview.tactic = tclUNIT () end) +[%%if coq = "8.18" || coq = "8.19"] let command_focus = Proof.new_focus_kind () +[%%else] +let command_focus = Proof.new_focus_kind "vscoq_command_focus" +[%%endif] let worker_solve_one_goal { TacticJob.state; ast; goalno; goal } ~send_back = let focus_cond = Proof.no_cond command_focus in diff --git a/language-server/dm/searchQuery.ml b/language-server/dm/searchQuery.ml index 50ce2fbe6..803f2789a 100644 --- a/language-server/dm/searchQuery.ml +++ b/language-server/dm/searchQuery.ml @@ -15,8 +15,7 @@ open Util open Printer open Protocol.Printing open Protocol.LspWrapper -open Vernacexpr -open Pp + (* Note: this queue is not very useful today, as we process results in the main vscoq process, which does not allow for real asynchronous processing of results. *) let query_results_queue = Queue.create () @@ -24,6 +23,9 @@ let query_results_queue = Queue.create () let query_feedback : notification Sel.Event.t = Sel.On.queue query_results_queue (fun x -> QueryResultNotification x) +[%%if coq = "8.18"] +open Vernacexpr +open Pp (* TODO : remove these two functions when interp_search_restriction is added in the comSearch.mli in Coq (they're simply copied here for now) *) let global_module qid = @@ -34,20 +36,25 @@ let global_module qid = let interp_search_restriction = function | SearchOutside l -> (List.map global_module l, true) | SearchInside l -> (List.map global_module l, false) +let adapt_pr_search f r k e c = f r k e (Evd.from_env e) c +[%%else] +let interp_search_restriction = ComSearch.interp_search_restriction +let adapt_pr_search f = f +[%%endif] let interp_search ~id env sigma s r = - let pr_search ref _kind env c = - let name = pr_global ref in + let pr_search ref _kind env sigma c = + let pr = pr_global ref in let open Impargs in let impls = implicits_of_global ref in let impargs = select_stronger_impargs impls in let impargs = List.map binding_kind_of_status impargs in - let statement = pr_ltype_env env Evd.(from_env env) ~impargs c in - let name = pp_of_coqpp name in - let statement = pp_of_coqpp statement in + let pc = pr_ltype_env env sigma ~impargs c in + let name = pp_of_coqpp pr in + let statement = pp_of_coqpp pc in Queue.push { id; name; statement } query_results_queue in let r = interp_search_restriction r in - (Search.search env sigma (List.map (ComSearch.interp_search_request env Evd.(from_env env)) s) r |> - Search.prioritize_search) pr_search; + (Search.search env sigma (List.map (ComSearch.interp_search_request env sigma) s) r |> + Search.prioritize_search) (adapt_pr_search pr_search); [query_feedback] diff --git a/language-server/dm/searchQuery.mli b/language-server/dm/searchQuery.mli index 5818b5962..e44a51087 100644 --- a/language-server/dm/searchQuery.mli +++ b/language-server/dm/searchQuery.mli @@ -15,6 +15,7 @@ open Protocol.LspWrapper val query_feedback : notification Sel.Event.t +[%%if coq = "8.18"] val interp_search : id:string -> Environ.env -> @@ -22,3 +23,12 @@ val interp_search : (bool * Vernacexpr.search_request) list -> Vernacexpr.search_restriction -> notification Sel.Event.t list +[%%else] +val interp_search : + id:string -> + Environ.env -> + Evd.evar_map -> + (bool * Vernacexpr.search_request) list -> + Libnames.qualid list Vernacexpr.search_restriction -> + notification Sel.Event.t list +[%%endif] diff --git a/language-server/language/dune b/language-server/language/dune index aad9afdda..5c69f412e 100644 --- a/language-server/language/dune +++ b/language-server/language/dune @@ -1,4 +1,5 @@ (library (name language) (public_name vscoq-language-server.language) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) (libraries coq-core.sysinit lsp)) \ No newline at end of file diff --git a/language-server/language/hover.ml b/language-server/language/hover.ml index add6da727..ec205be80 100644 --- a/language-server/language/hover.ml +++ b/language-server/language/hover.ml @@ -38,9 +38,31 @@ let compactify s = List.fold_left (fun s (reg,repl) -> Str.global_replace reg repl s) s replacements (* TODO this should be exposed by Coq and removed from here *) + +[%%if coq = "8.18"] +let pr_s = prlist (fun CAst.{v=s} -> str "%" ++ str s) +let eq_realarg = List.equal (fun a b -> String.equal a.CAst.v b.CAst.v) +let nargs_maximal_of_pos ((na,_,_),_,(maximal,_)) = na, maximal +let make_scope = CAst.make +[%%else] +let pr_delimiter_depth = function + | Constrexpr.DelimOnlyTmpScope -> str "%_" + | Constrexpr.DelimUnboundedScope -> str "%" +let pr_scope_delimiter (d, sc) = pr_delimiter_depth d ++ str sc +let pr_s = prlist (fun CAst.{v=s} -> pr_scope_delimiter s) + +let eq_realarg = + List.equal + (fun a b -> let da, a = a.CAst.v in let db, b = b.CAst.v in + da = db && String.equal a b) +let nargs_maximal_of_pos imp = + let (na, _, _) = imp.Impargs.impl_pos in + na, imp.Impargs.impl_max +let make_scope = (fun s -> CAst.make (Constrexpr.DelimUnboundedScope, s)) +[%%endif] + let pr_args args more_implicits mods = let open Vernacexpr in - let pr_s = prlist (fun CAst.{v=s} -> str "%" ++ str s) in let pr_if b x = if b then x else str "" in let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in let pr_br imp force x = @@ -56,8 +78,7 @@ let pr_args args more_implicits mods = if s = [] && imp = Glob_term.Explicit then [], tl else let rec fold extra = function - | RealArg arg :: tl when - List.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s + | RealArg arg :: tl when eq_realarg arg.notation_scope s && arg.implicit_status = imp -> fold ((arg.name,arg.recarg_like) :: extra) tl | args -> List.rev extra, args @@ -99,7 +120,9 @@ let pr_args args more_implicits mods = let implicit_kind_of_status = function | None -> Anonymous, Glob_term.Explicit - | Some ((na,_,_),_,(maximal,_)) -> na, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit + | Some imp -> + let na, maximal = nargs_maximal_of_pos imp in + na, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit let extra_implicit_kind_of_status imp = let _,imp = implicit_kind_of_status imp in @@ -131,7 +154,7 @@ let rec main_implicits i renames recargs scopes impls = | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit) in let notation_scope = match scopes with - | scope :: _ -> List.map CAst.make scope + | scope :: _ -> List.map make_scope scope | [] -> [] in let status = {Vernacexpr.implicit_status; name; recarg_like; notation_scope} in @@ -166,14 +189,26 @@ let rec insert_fake_args volatile bidi impls = let f = Option.map pred in RealArg hd :: insert_fake_args (f volatile) (f bidi) tl +[%%if coq = "8.18"] +let ref_of_const x = Some x +[%%else] +let ref_of_const = function +| GlobRef.ConstRef ref -> Some ref +| _ -> None +[%%endif] + let print_arguments ref = let flags, recargs, nargs_for_red = let open Reductionops.ReductionBehaviour in - match get ref with + match ref_of_const ref with + | Some ref -> + begin match get ref with + | None -> [], [], None + | Some NeverUnfold -> [`ReductionNeverUnfold], [], None + | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs + | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs + end | None -> [], [], None - | Some NeverUnfold -> [`ReductionNeverUnfold], [], None - | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs - | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs in let names, not_renamed = try Arguments_renaming.arguments_names ref, false @@ -260,4 +295,4 @@ let get_hover_contents env sigma ref_or_by_not = end in Option.map Lsp.Types.(fun value -> MarkupContent.create ~kind:MarkupKind.Markdown ~value) r - | Constrexpr.ByNotation (_ntn,_sc) -> assert false \ No newline at end of file + | Constrexpr.ByNotation (_ntn,_sc) -> assert false diff --git a/language-server/vscoq-language-server.opam b/language-server/vscoq-language-server.opam index ba508be1e..9a7e05c9b 100644 --- a/language-server/vscoq-language-server.opam +++ b/language-server/vscoq-language-server.opam @@ -12,9 +12,9 @@ build: [ ] depends: [ "ocaml" { >= "4.13.1" } - "dune" { >= "3.2" } - "coq-core" { >= "8.18" < "8.19" } - "coq-stdlib" { >= "8.18" < "8.19" } + "dune" { >= "3.5" } + "coq-core" { >= "8.18" < "8.20" } + "coq-stdlib" { >= "8.18" < "8.20" } "yojson" "jsonrpc" { >= "1.15"} "ocamlfind" @@ -26,6 +26,7 @@ depends: [ "sexplib" "ppx_yojson_conv" "ppx_import" + "ppx_optcomp" "result" { >= "1.5" } "lsp" { >= "1.15"} "sel" {>= "0.4.0"}