coq / vscoq

Visual Studio Code extension for Coq
MIT License
337 stars 69 forks source link

Compiled library ... makes inconsistent assumptions #686

Closed kylechui closed 11 months ago

kylechui commented 11 months ago

I installed VSCoq2 and it keeps throwing this error on my end, even though running make clean; make CoqMakefile; make runs everything without any issues (other than some deprecation warnings). I'm running everything on NixOS and have it installed via the Nix flake; the version of Coq and VSCoq are both 8.18.0 (which seems to be the latest version). The language server seems to work just fine for certain files in my project, but for other ones it shows the "inconsistent assumptions" error. From what I gather by looking the error up online it's related to mismatched Coq versions between compiled code vs. source code. Any thoughts appreciated!

So far, I've checked:

I'm running things on Neovim, using the vscoq.nvim plugin. I imagine the issue should be with the language server itself, and not the client, but can migrate the issue if necessary. Thanks in advance!

image

Maybe not the most effective way to do things, but here's the flake:

{
  description = "Local development environment for 2ControlVerification";
  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
    vscoq.url = "github:coq-community/vscoq";
  };

  outputs = { self, nixpkgs, vscoq }:
    let
      system = "x86_64-linux";
      pkgs = nixpkgs.legacyPackages.${system};
      vscoq-language-server = vscoq.packages.${system};
    in {
      devShell.${system} = pkgs.mkShell {
        nativeBuildInputs =
          [ pkgs.coq_8_18 vscoq-language-server.vscoq-language-server ];
      };
    };
}
kylechui commented 11 months ago

I switched to using Coqtail