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.

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

[2023.11] [coq-lsp 0.2.0] [v8.19] Draft Windows build #399

Draft
wants to merge 4 commits into
base: main
Choose a base branch
from

Conversation

ejgallego
Copy link
Member

Changes:

  • Simplify some paths and logic
  • Updated for 8.19

@ejgallego ejgallego force-pushed the coq_lsp_8_19 branch 4 times, most recently from 1d85f0b to 3f21e1f Compare February 8, 2024 21:23
@MSoegtropIMC
Copy link
Collaborator

@ejgallego : anything I can help with?

@ejgallego ejgallego force-pushed the coq_lsp_8_19 branch 2 times, most recently from b84600a to 64729af Compare February 9, 2024 12:04
@ejgallego
Copy link
Member Author

@ejgallego : anything I can help with?

Everything good, thanks! I started with the 8.19 pick, but indeed had to remove a few broken contribs. The installer seems to work good now, and it is simpler than in previous versions as I didn't have to patch Coq this time.

@MSoegtropIMC
Copy link
Collaborator

Are you using the installer in a lecture?

@ejgallego
Copy link
Member Author

This particular artifact hasn't been tested yet, however the artifacts for 8.17 / 8.18 have been used by quite a few people with pretty good results I understand, including lectures.

@ejgallego
Copy link
Member Author

Artifact tested, working pretty well on the cases we have.

[Note that the current installer still requires to config VSCode as outline in the README on coq-lsp for Windows]

@ejgallego ejgallego changed the title [2023.11] [coq-lsp 0.1.8] [v8.19] Draft Windows build [2023.11] [coq-lsp 0.1.9] [v8.19] Draft Windows build May 31, 2024
@ejgallego ejgallego force-pushed the coq_lsp_8_19 branch 2 times, most recently from 407c024 to 6f081b6 Compare June 3, 2024 16:40
@ejgallego ejgallego force-pushed the coq_lsp_8_19 branch 2 times, most recently from 9744523 to 7d35d38 Compare September 9, 2024 12:44
@ejgallego ejgallego changed the title [2023.11] [coq-lsp 0.1.9] [v8.19] Draft Windows build [2023.11] [coq-lsp 0.2.0] [v8.19] Draft Windows build Sep 9, 2024
@ejgallego ejgallego force-pushed the coq_lsp_8_19 branch 2 times, most recently from f8724ba to 4714da1 Compare September 9, 2024 13:38
@ejgallego
Copy link
Member Author

@MSoegtropIMC , actually there is something strange going on here (and in the sister PRs for 8.18 and 8.17) , for some reason, CoqIDE is not building correctly, I am not sure why, it seems the custom repos logic is working as intended.

@MSoegtropIMC
Copy link
Collaborator

@ejgallego : as you might remember we always had a patched lablgtk in Windows + a few matching patches in CoqIDE. Recently this was fixed up in lablgtk upstream which requires adjustments in CoqIDE. The errors I see are in this area - I would say the patch level of CoqIDE doesn't match the version of lablgtk used. Which one is wrong is hard to tell, but I guess CoqIDE patches are missing.

@MSoegtropIMC
Copy link
Collaborator

Btw.: I made good progress with solving the path length issue permanently. The manifest changes work fine, I just need a reliable automation for the registry change (especially on GIT runners).

@ejgallego
Copy link
Member Author

Which one is wrong is hard to tell, but I guess CoqIDE patches are missing.

Indeed, it seems like CoqIDE patches not being applied, however the local repos seems setup correctly, bizarre.

@MSoegtropIMC
Copy link
Collaborator

MSoegtropIMC commented Sep 10, 2024

This issue is that you have "coqide.8.19.0" but an opam package with the patch exists only for coqide.8.19.2.

@MSoegtropIMC
Copy link
Collaborator

I need to merge this upstream for all versions, but too busy with other loose ends ...

@ejgallego
Copy link
Member Author

This issue is that you have "coqide.8.19.0" but an opam package with the patch exists only for coqide.8.19.2.

Thanks @MSoegtropIMC , where do you see "coqide.8.19.0", I see instead:

PACKAGES="${PACKAGES} coqide.8.19.2"

I need to merge this upstream for all versions, but too busy with other loose ends ...

I will be happy to help with that, just give me a heads up when you want this to land in the main branch.

The setup is now standard, just adding coq-lsp to PACKAGES will do the trick.

Note that however it is strongly recommended to run the +lsp Coq branches, due to critical patches for UI stability.

@MSoegtropIMC
Copy link
Collaborator

Yes, sorry - I somehow ended up browsing the initial commit where it was 8.19.0. The latest commit is indeed 8.19.2. I need to do a local test.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants