Skip to content

Conversation

@ejgallego
Copy link
Member

This is needed by SerAPI, coq-lsp, and likely others.

Looking at git history, it seems this package was added to this list by mistake. Confirmed to fix problems of coq-lsp / SerAPI in Windows.

This is needed by SerAPI, coq-lsp, and likely others.

Looking at git history, it seems this package was added to this list
by mistake. Confirmed to fix problems of `coq-lsp` / `SerAPI` in
Windows.
@ejgallego
Copy link
Member Author

Snap build failed due to out of disk error, rest looks fine, testing looks fine here too.

@ejgallego
Copy link
Member Author

@MSoegtropIMC is there anything blocking this?

@MSoegtropIMC
Copy link
Collaborator

@ejgallego : no. It is just so that the release happens in phases. First we (mostly) reconstruct the previous release with updated coq and packages. Then we look into changes.

@ejgallego
Copy link
Member Author

Thanks for the info! Is there a milestone / tag that we could use to mark PRs that we'd like to be considered for inclusion in the next release (and not related to the package pick per-se) ?

@MSoegtropIMC
Copy link
Collaborator

@ejgallego : thanks! I cherry picked this into my release prep branch msoegtrop/prepape-2023.11-3 (for efficiency - CI takes hours), so I close this PR.

@ejgallego ejgallego deleted the recover_sexplib0 branch January 15, 2024 13:36
@ejgallego
Copy link
Member Author

Thanks @MSoegtropIMC !

IIUC the fix will be propagated back to the 8.17 versions of the platform, correct?

@MSoegtropIMC
Copy link
Collaborator

We would have to create and sign new installers, which is a substantial effort - you have to ask e.g. Maxime if he wants to go through this.

Using the scripts was btw. never affected by this, just binary installers.

Btw.: I now added a smoke test for coq-serapi:

echo '(Add () "Lemma addn0 n : n + 0. Proof. now induction n. Qed.") (Exec 5)' | sertop

I hope this is reasonable.

@ejgallego
Copy link
Member Author

The test looks good!

Using the scripts was btw. never affected by this, just binary installers.

Indeed my use case is building the custom binary installers for coq-lsp users, as done in #368 and #369 .

I understand I still need to keep the patch on these branches that are based on main, or will you merge the prepape-2023.11-3 branch to main at some point?

@MSoegtropIMC
Copy link
Collaborator

The prepare-2023.11-3 will be merged to main as soon as CI passes (and I will tag then).

The installer creation scripts are shared between all picks, so when you create a custom pick you have this.

coq-lsp as such will likely be included in a soon to come 2023.11.1 release. 2023.11.0 just updates and solves all technical issues - new stuff comes in a separate release.

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