Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
andreykl opened this issue Dec 6, 2021 · 2 comments

Comments

@andreykl
Copy link
Contributor

andreykl commented Dec 6, 2021

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
Copy link
Contributor Author

andreykl commented Dec 6, 2021

or better

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

@gares
Copy link
Member

gares commented Dec 7, 2021

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants