Coq

Code like

have {H}H : ...

triggers a cryptic warning. It should suggest to write

have {}H : ...

instead.

See also: https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/duplicate.20clear

There is now a type circle in UniMath.SyntheticHomotopyTheory.Circle2. It would be great to define pi_1 of a pointed type, and to show that pi_1(circle, pt) \simeq Z.

• obtaining the highest level of common criteria certification

最高等级的通用准则认证(common criteria certification)

这里 certification 译为认证可能更合适，因为是政府机构签发的，见：
https://www.commoncriteriaportal.org/files/ppfiles/pp0099V2a_pdf.pdf
http://www.uscxm.com/Chinese/news/2020/20200108.asp

• As an environment for developing formally certified software and hardware,

漏了硬件，另外 certified 和 verified 是否要在中文中

I won't have time to implement this, but it should be easy and it should provide a nice quality of life improvement.

Each goal buffer stars with a header line, like this:

1 focused subgoal
(shelved: 1) (ID 339)
  
  width : Z
  BW : Bitwidth width
  …

It would be nice to move that info to the modeline, next to the buffer name (*goals*). We can change the "lighter" of the

I've noticed that even with the fastest reduction strategy available - lazy - running tmEval within the TemplateMonad is still much slower than vm_compute. I have an example for which tmEval lazy takes around 22 sec, and vm_compute finishes in 4.5 sec.

Is there a way of using vm_compute for reduction?

Characters like (space) are not allowed for .v files, but vscoq does not give any useful error message and just hangs if accidently called on such files. Same for file names with empty name (filename just .v, happens occasionally when i hit some shortcut by accident).

Eval cbn in 1 + 1.
Definition x :=
  Eval cbn in 1 + 1.
Definition y := 2.

The second Eval is not highlighted, and the second Definition is indented to match the second Eval.