Axiom - Professional Rocq IDE

Announcements
1

Hi everyone,

We’re building Axiom, with the goal of becoming a strong, fast, and feature rich IDE for Rocq, suitable for all scales of development, from hobby and small all the way up to enterprise level projects.

Besides the essentials like Goals, Proof View, etc., we’re actively developing the following:

  • Frictionless project-bound, fully reproducible environments
  • Project-scale navigation (workspace + dependencies) and indexing
  • High focus on reliability, 0 hangs/crashes policy
  • Ergonomic UI
  • Proof diff viewer, not just “text diff”
  • Semantic refactoring and search
  • Proof-state instrumentation and flight-recorder for large projects
  • Wiki support for coqdoc
  • and more.

Our mission for v1 is to provide much more value than typical setups with VSCode, (Neo)Vim, and Emacs out of the box.

We aim during development for weekly update cycles. At some point we would offer Axiom as a 3-tier model: Free, Pro, Enterprise. A mid to long term plan is to also support other ecosystems such as Lean.

We’d also value input from active Rocq users on what costs you time and energy today. Concretely:

  • What breaks your flow most often?
  • What’s the most painful workflow you repeat often?
  • If you could “buy” one IDE capability, what would it be?
  • What is your current setup?
  • If you could imagine any feature / capability, what would it be.

Thank you very much for your attention and feedback. We’re very excited about this and we’re looking forward to work close with the community!

2

My current set up is VsCode for a single reason I do not want one more IDE. I want a multi-purposed one because like many people I don’t work with project consist of Rocq files. I also need support for Ocaml, Latex, and a bunch of other languages. And often I have both ocaml and rocq code open at the same time, or keep switching between them. While I agree much better support is needed, one more IDE does not interest me. Having to step up and learn n-IDE is the worst, and this why VsCode, Emacs, Vim and so on are so popular.

Can’t this be done as a paying extension in VsCode like many others like gitlens ?
Lean’s one works great, for instance. Agda one for Emacs is great too.

1 Like
3

Hi @thomas-lamiaux , thanks for your reply. Ideally we would like to be vertically integrated and own the entire experience a-la-JetBrains, but a paid VSCode extension could be a viable solution to some of the things we want to offer, we’re actively weighting that option too. It would be great if you could also let us know what are some features / capabilities you’d like to see that are currently non-existent.

4

We can set up a visio next week if you wish to discuss specifics, you can contact me at thomas.lamiaux@inira.fr

1 Like
5

I suppose most people learn their first IDE in their teens, and once that happens, the cost/benefit analysis argues against learning any more than you have to. For me, that IDE was emacs (the year was 1994 …), and for kids these days, it seems to be VSCode. However, for a few specific audiences, a specialized Rocq IDE would be useful. I am thinking in particular of the students in my first-year university classes, who are typically in their teens. Many of them have not yet settled on an IDE for life. To ask them all to use VSCode (or emacs, or vim, or whatever) seems a bit premature – I’m not sure how well I would have taken to an IDE if the choice had been forced upon me instead of being a choice that I made of my own free will. All I really need here is something lightweight and better than CoqIDE, which is a pretty low bar. If a student already knows VSCode or emacs and wants to use it, they are still free to do so, but for everyone else, it would be useful to have a dedicated IDE.

I’m not so enamored of the paid extension idea, though. Free and open source is a baseline requirement.

1 Like
6

Proof diff viewer, not just “text diff”

How is the “proof diff viewer” different/better than the current proof diff feature?

1 Like
7

We’d add:

  • Proof-state timeline (“flight recorder”):
    • A clickable timeline of commands/sentences with captured proof-state snapshots
    • Lets you jump back to understand where the proof state diverged which could be useful for debugging and refactors
  • Independent point in time diff:
    • Diff any two points in the proof session: step N vs step M, “before tactic X” vs “after tactic Y”
8

Hi @davidjao , thanks for your reply. The switching cost is indeed real, we don’t want to approach building an IDE as a “general IDE” like VSCode or JetBrains, our mid to long term is to cover niche languages such as Agda, Lean, Rocq, Haskell, OCaml, Erlang, etc., as we believe those ecosystems are vastly under developed and tooling lacks significantly. We thought a good wedge to start is Rocq.

We also think that creating an extension will be unavoidable due to the vast audience that has strong ties to VSCode already. To ensure both can be delivered with the quality we want, besides the free tier, there needs to be a paid tier. We don’t want to take VC money or any other intrusive investment as we think it will just create the wrong incentives and hurt the communities instead. We believe that fair and honest pricing, paired with strong community engagement, open roadmaps and open governance, are the right way to go for these ecosystems.

With that said, teaching institutions are also a place we’d like to go into. From your perspective, what are workflows / features that you believe are important to have or that would be great time savers for you and your students?

10

Hi @thomas-lamiaux , I sent you an email on Sunday but yesterday it bounced back, could it have been filtered for spam?