search

toku-sa-n / coqfmt

Coq code formatter
https://toku-sa-n.github.io/coqfmt/
GNU Affero General Public License v3.0
21 stars 2 forks source link

Import not implemented #519

Open womeier opened 2 weeks ago

womeier commented 2 weeks ago 
From Coq Require Import Uint63.

Eval cbn in (Uint63.addmuldiv 4611686018427387904 1 1).

Eval native_compute in (Uint63.addmuldiv 4611686018427387904 1 1).

Eval vm_compute in (Uint63.addmuldiv 4611686018427387904 1 1).

gives the error:

Fatal error: exception Coqfmt__Ppast.Not_implemented("From Coq Require Import Uint63.\n\n")

I'm using version 4da8795.

Wouldn't it be possible to pretty-print unsupported constructs as in the input file?

toku-sa-n commented 2 weeks ago

Sorry for the late response. This misleading exception contains the code that Coqfmt could format. For this case, Coqfmt hasn't been implemented pretty-printing the Eval line. I'll implement it later.

I'm sorry, but it is difficult to implement Coqfmt to print the same thing as the input for this kind of case.