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

Evolve learn tabs #60

Merged
merged 4 commits into from
Jan 20, 2025
Merged

Evolve learn tabs #60

merged 4 commits into from
Jan 20, 2025

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Jan 16, 2025

This implements what was discussed during yesterday's meeting. This is on top of #59. Bikeshedding is authorized for the name of the "Rocq Prover and Platform features" tab (should it just be "Platform Docs" or "Features"?) and the "Supporting tools" tab.

The "Supporting tools" tab is a bit dry for now. In an upcoming (draft) PR, I attempt to fill it with existing guides from coq.inria.fr.

@Zimmi48 Zimmi48 mentioned this pull request Jan 16, 2025
@mattam82 mattam82 changed the base branch from main to staging January 20, 2025 10:48
@mattam82 mattam82 merged commit 18e7d3b into staging Jan 20, 2025
3 checks passed
@mattam82
Copy link
Member

mattam82 commented Jan 20, 2025

@Zimmi48 @BastienSozeau how about tabs (link for the platforms on the left) for the different editors to quickly jump (and get at a glance all the available options). The current state with evolve-lear merged is here:
https://staging.rocq-prover.org/install#mac

@Zimmi48
Copy link
Member Author

Zimmi48 commented Jan 20, 2025

We discussed this option during the meeting last Wednesday, but we decided that tabs by operating system allowed to show OS-specific information about editors, and that this was better. Of course, it is still possible to revisit this decision (if I'm not the one to do the work 😉).

@mattam82
Copy link
Member

I don't think that's incompatible, I would just like to see below "Set Up Your Editor" a list of links to all the editors available for the current chosen platform

@mattam82
Copy link
Member

In any case, the proposed changes are already better than what we had, so I'll push to main

@Zimmi48
Copy link
Member Author

Zimmi48 commented Jan 20, 2025

I don't think that's incompatible, I would just like to see below "Set Up Your Editor" a list of links to all the editors available for the current chosen platform

OK, that's very do-able, I think.

@Zimmi48 Zimmi48 deleted the evolve-learn branch January 20, 2025 13:41
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