Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix for prior versions of Coq #946

Merged
merged 3 commits into from
Nov 22, 2024
Merged

Fix for prior versions of Coq #946

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8eb8c57
fix: update flake to have git in dev shell
rtetley Nov 19, 2024
0454b11
fix: fix lspManager for prior versions of coq (8.18, 8.19, 8.20) and …
rtetley Nov 19, 2024
0f0f29b
fix: flake file clean up and ci fixes
rtetley Nov 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ jobs:
fail-fast: false
matrix:
os: [ubuntu-latest, macos-latest]
coq: [coq-8-18, coq-8-19, coq-master]
coq: [8-18, 8-19, 8-20, master]
profile: [dev, fatalwarnings]
runs-on: ${{ matrix.os }}
steps:
Expand All @@ -53,11 +53,11 @@ jobs:
diff new_yarn.nix yarn.nix
diff goal-view-ui/new_yarn.nix goal-view-ui/yarn.nix
diff search-ui/new_yarn.nix search-ui/yarn.nix
- run: nix develop .#vscoq-language-server-${{ matrix.coq }} -c bash -c "cd language-server && dune build --profile ${{ matrix.profile }}"
- 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"
- run: nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd language-server && dune build --profile ${{ matrix.profile }}"
- run: nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd client && yarn run install:all && yarn run build:all && yarn run compile"
- run: xvfb-run nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd client && yarn test"
if: runner.os == 'Linux'
- run: nix develop .#vscoq-client -c bash -c "cd client && yarn test"
- run: nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd client && yarn test"
if: runner.os != 'Linux'
- if: ${{ failure() }}
run: cat /tmp/vscoq_init_log.*
Expand All @@ -68,7 +68,7 @@ jobs:
matrix:
os: [ubuntu-latest]
ocaml-compiler: [4.14.x]
coq: [8.18.0, 8.19.0, 8.20+rc1, dev]
coq: [8.18.0, 8.19.0, 8.20.0, dev]
runs-on: ${{ matrix.os }}
steps:
- name: Checkout
Expand Down
2 changes: 2 additions & 0 deletions client/src/test/suite/extension.test.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ suite('Should get diagnostics', function () {

const ext = vscode.extensions.getExtension('maximedenes.vscoq')!;
await ext.activate();
vscode.workspace.getConfiguration().update('vscoq.proof.mode','Continuous');

const doc = await common.openTextFile('basic.v');

Expand All @@ -34,6 +35,7 @@ suite('Should get diagnostics', function () {

const ext = vscode.extensions.getExtension('maximedenes.vscoq')!;
await ext.activate();
vscode.workspace.getConfiguration().update('vscoq.proof.mode','Continuous');

const doc1 = await common.openTextFile('basic.v');
const doc2 = await common.openTextFile('warn.v');
Expand Down
73 changes: 44 additions & 29 deletions flake.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
formatter = nixpkgs.legacyPackages.${system}.alejandra;

packages = {
default = self.packages.${system}.vscoq-language-server-coq-8-19;
default = self.packages.${system}.vscoq-language-server-coq-8-20;

vscoq-language-server-coq-8-18 =
# Notice the reference to nixpkgs here.
Expand All @@ -52,9 +52,8 @@
gnome.adwaita-icon-theme
wrapGAppsHook
ocaml
yojson
zarith
findlib
yojson
ppx_inline_test
ppx_assert
ppx_sexp_conv
Expand All @@ -66,6 +65,10 @@
lsp
sel
]);
propagatedBuildInputs= (with coq.ocamlPackages;
[
zarith
]);
};

vscoq-language-server-coq-8-19 =
Expand Down Expand Up @@ -93,7 +96,6 @@
wrapGAppsHook
ocaml
yojson
zarith
findlib
ppx_inline_test
ppx_assert
Expand All @@ -106,6 +108,10 @@
lsp
sel
]);
propagatedBuildInputs= (with coq.ocamlPackages;
[
zarith
]);
};

vscoq-language-server-coq-8-20 =
Expand Down Expand Up @@ -133,7 +139,6 @@
wrapGAppsHook
ocaml
yojson
zarith
findlib
ppx_inline_test
ppx_assert
Expand All @@ -146,6 +151,10 @@
lsp
sel
]);
propagatedBuildInputs= (with coq.ocamlPackages;
[
zarith
]);
};

vscoq-language-server-coq-master =
Expand Down Expand Up @@ -173,7 +182,6 @@
wrapGAppsHook
ocaml
yojson
zarith
findlib
ppx_inline_test
ppx_assert
Expand All @@ -186,6 +194,10 @@
lsp
sel
]);
propagatedBuildInputs= (with coq.ocamlPackages;
[
zarith
]);
};

vscoq-client = with import nixpkgs {inherit system;}; let
Expand Down Expand Up @@ -267,64 +279,67 @@
};

devShells = {
vscoq-client = with import nixpkgs {inherit system;};
mkShell {
buildInputs = self.packages.${system}.vscoq-client.extension.buildInputs;
};

vscoq-language-server-coq-8-18 = with import nixpkgs {inherit system;}; let
ocamlPackages = ocaml-ng.ocamlPackages_4_14;
in
vscoq-8-18 = with import nixpkgs {inherit system;};
mkShell {
buildInputs =
self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs
buildInputs =
self.packages.${system}.vscoq-client.extension.buildInputs
++ self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs
++ (with ocamlPackages; [
ocaml-lsp
]);
])
++ ([git]);
};

vscoq-language-server-coq-8-19 = with import nixpkgs {inherit system;}; let
vscoq-8-19 = with import nixpkgs {inherit system;}; let
ocamlPackages = ocaml-ng.ocamlPackages_4_14;
in
mkShell {
buildInputs =
self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs
self.packages.${system}.vscoq-client.extension.buildInputs
++ self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs
++ (with ocamlPackages; [
ocaml-lsp
]);
])
++ ([git]);
};

vscoq-language-server-coq-8-20 = with import nixpkgs {inherit system;}; let
vscoq-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
self.packages.${system}.vscoq-client.extension.buildInputs
++ self.packages.${system}.vscoq-language-server-coq-8-20.buildInputs
++ (with ocamlPackages; [
ocaml-lsp
]);
])
++ ([git]);
};

vscoq-language-server-coq-master = with import nixpkgs {inherit system;}; let
vscoq-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
self.packages.${system}.vscoq-client.extension.buildInputs
++ self.packages.${system}.vscoq-language-server-coq-master.buildInputs
++ (with ocamlPackages; [
ocaml-lsp
]);
])
++ ([git]);
};

default = with import nixpkgs {inherit system;}; let
ocamlPackages = ocaml-ng.ocamlPackages_4_14;
in
mkShell {
buildInputs =
self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs
self.packages.${system}.vscoq-client.extension.buildInputs
++ self.packages.${system}.vscoq-language-server-coq-8-20.buildInputs
++ (with ocamlPackages; [
ocaml-lsp
]);
])
++ ([git]);
};
};
});
Expand Down
16 changes: 15 additions & 1 deletion language-server/vscoqtop/lspManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -268,6 +268,19 @@ let init_document local_args vst =
Vernacstate.freeze_full_state ()
[%%endif]

[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
let parse_args args =
let usage = {
Boot.Usage.executable_name = "";
extra_args = "";
extra_options = "";
} in
fst @@ Coqargs.parse_args ~init:Coqargs.default ~usage args
[%%else]
let parse_args args =
fst @@ Coqargs.parse_args ~init:Coqargs.default args
[%%endif]

let open_new_document uri text =
let vst = get_init_state () in

Expand All @@ -282,7 +295,8 @@ let open_new_document uri text =
let project = CoqProject_file.read_project_file ~warning_fn:(fun _ -> ()) f in
let args = CoqProject_file.coqtop_args_from_project project in
log (Printf.sprintf "Arguments from project file %s: %s" f (String.concat " " args));
fst @@ Coqargs.parse_args ~init:Coqargs.default args
parse_args args

in

let vst = init_document local_args vst in
Expand Down
Loading