Rocq FAQ

Does Rocq support Unicode?

Yes it does. In fact, you don’t need to do anything, and you will be able to use Unicode in notations.

Caution

Certain Unicode characters are seen as letters, and only those can be used inside identifiers. For Rocq Notations however you are free to use them however you want.

You can actually even use ∀ (x : A), B instead of forall (x : A), B, A ∧ B instead of A /\ B, A → B instead of A -> B and so on… as soon as you import the Utf8 module:

From Rocq Require Import Utf8.

Tip

You can use the latex-input VSCode extension (or presumably others of your liking) to enter Unicode characters easily.

Do I really have to manually evaluate each line when navigating a Rocq file?

Assuming you use RocqIDE or the default setting for VSRocq, then the answer is mostly yes. However, you can also tell Rocq to evaluate up to the point where your cursor is. In VSRocq you do it with Ctrl + Alt + → or “Interpret to point” from the commande palette (Ctrl + Shift + P).

In VSRocq, you also have access to “Continuous mode” which displays the goal where your cursor is, and otherwise evaluates everything in the background. Use at your own risks though, this feature has been experiencing bugs in the past. See our section on editors for more.

Why can’t I use a dash (-) in the filename?

Rocq doesn’t let you use dashes in the filename (for instance if you call it my-file.v then VSRocq will not work) because implicitly, a filename becomes a Rocq module name (a bit like OCaml files become OCaml modules). So myFile.v will become the myFile module, and those don’t allow for dashes in them. In fact, it’s better to stick to letters and underscores (_).

Note

There’s no need to understand all this, just know that if Rocq won’t even start then it’s a good idea to try for a simpler name, just in case.

I’m testing my own tactic and I would like to know how long it takes, how can I do that?

If you want to know how long a tactic or a command takes, you can use the Time command for instance as follows:

Time my_tactic.

or even

Time Qed.

Wait, wasn’t Rocq called Coq? What’s the difference?

Indeed, Rocq was formerly known as Coq, you can read more about it on the official website.

Can I use Nix to install Rocq and MetaRocq?

Nix can be used to install Rocq and Equations, as well as many other packages, but it seems to be currently broken when it comes to MetaRocq so unless you want to spend hours debugging things, we recommend you use opam or the binary installers as advised in the installation page.

Is it possible to simplify only parts of an expression?

If simpl simplifies too much, you can also use eg. simpl add to only simplify addition. So for instance (0 + S n) - m will become S n - m without Rocq unfolding also -.

You will see in lesson 3 a bit more about computation and how to control it.

How do I use multiple files in a project?

If you want to have a multi-file project, you need to create a _RocqProject file (with exactly this name and no extension) at the root of your directory (the one you open eg. with VSRocq) of the following shape.

-Q . ProjectName

ex1.v
ex2.v
ex3.v
a_folder_with_v_files_I_dont_want_to_list_manually

It lists all the files (or path to files if not in the same directory) and of directories (in which case it will compile all .v files in it) and gives a name to the project (here: ProjectName).

Note

You don’t need to put then in any particular order, but it’s usually nicer to have them in dependency order.

Then in one of the files you can import, eg, the definitions from ex1.v by writing

From ProjectName Require Import ex1.

Note

The .v is removed from the name here.

You can then build your project by using the following Makefile.

all: Makefile.rocq
    $(MAKE) -f Makefile.rocq

clean: Makefile.rocq
    $(MAKE) -f Makefile.rocq clean

Makefile.Rocq:
    rocq makefile -f _RocqProject -o Makefile.rocq

.PHONY: all clean

Running make is then going to build all your project. And you might need to run make again after an update to see it happen in RocqIDE or VSRocq.

Important

Make sure that the Makefile uses tabs and not spaces, otherwise it may not work.