search

math-comp / mcb

Mathematical Components (the Book)
Other
140 stars 25 forks source link

comment search in snippets because it is too slow for jscoq and leave warning #141

Open andreykl opened 2 years ago

andreykl commented 2 years ago

comment search in snippets because it is too slow for jscoq and leave warning in example in ch2.v/ch2.html.

Search (odd _). Search eq odd -coprime.

should be kind of

( Search (odd _). ) ( Search eq odd -coprime. )

andreykl commented 2 years ago

or better

(* Warning: search code might be slow on some computers *)
(* when it is ran using jscoq *)
(* Search (odd _). *)
(* Search eq odd -coprime. *)
gares commented 2 years ago

I agree.

BTW, did you see this: https://github.com/jscoq/jscoq/blob/f4463b959686a13be404c53411f8497a958ece93/package.json.wacoq#L63 it is a bit faster, apparently, and you should be able to enable it by just replacing one line.