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

More sensible links for beginners installing Rocq. #37

Merged
merged 1 commit into from
Jan 2, 2025

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Jan 2, 2025

Link the Getting Started button to the Getting Started section in the doc. Stop pointing beginners at the opam tutorial and use the link to the install page more often.

In the future, the opam and switch tutorials should also be updated to be more alike the current https://coq.inria.fr/opam-using.html (maybe by simply reusing the content of this page instead of the current one that was adapted from the OCaml.org website).

@tabareau
Copy link
Contributor

tabareau commented Jan 2, 2025

with the refactoring, https://rocq-prover.org/install#rocq_platform is now empty, do we pick windows as default for the Rocq Platform ?

@Zimmi48
Copy link
Member Author

Zimmi48 commented Jan 2, 2025

No, the default is computed based on your operating system. You may have a strange behavior that is due to having visited the page before. Try removing the site data and re-browsing to this page. I just need to remove the anchor.

Link the Getting Started button to the Getting Started section in the doc.
Stop pointing beginners at the opam tutorial and use the link to the install page more often.
@Zimmi48 Zimmi48 force-pushed the link-to-install-page branch from e73bf49 to 336190e Compare January 2, 2025 16:39
@Zimmi48
Copy link
Member Author

Zimmi48 commented Jan 2, 2025

Link fixed.

@tabareau
Copy link
Contributor

tabareau commented Jan 2, 2025

Ok, I think we can merge now

@tabareau tabareau merged commit 7d09cd5 into main Jan 2, 2025
3 checks passed
@Zimmi48 Zimmi48 deleted the link-to-install-page branch January 2, 2025 16:44
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