Port Coq code to use 'done' tactic instead of 'easy' and benchmark

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

https://math-classes.github.io

MIT License

162 stars 43 forks source link

Port Coq code to use 'done' tactic instead of 'easy' and benchmark #129

Open ndcroos opened 3 months ago

ndcroos commented 3 months ago

See https://github.com/coq-community/math-classes/issues/128 See also this discussion: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Error.20in.20MathClasses.2C.20adding.20an.20import

Todo's:

benchmarking
hide fast_done

palmskog commented 3 months ago

@ndcroos the fast_done and done tactics are as far as I know independent of the rest of stdpp. So why do you need to bundle base.v? This is a big file with lots of choices in how to configure Coq, that will take quite a lot of time to maintain inside this project.

ndcroos commented 3 months ago

@palmskog I need base.v for not_symmetry. I still need to delete code in (mostly) base.v that is not needed.

ndcroos commented 3 months ago

I got a lot of errors executing make that are due to easy --> done changes, so I think it is makes more sense to revert all the easy --> done changes, and then doing them again one by one, while making sure that the project compiles. I also moved stdpp_tactics.v to the misc directory.

(It seems like perhaps the most straightforward changes are those were easy is the last step in the proof. But I am not sure of this.)

ndcroos commented 3 months ago

Files where replacing 'easy' didn't work:

theory/series
implementations/dyadics.v
misc/util.v (because of circular dependency)

spitters commented 2 months ago

Thanks @ndcroos ! What's the status of this?

ndcroos commented 2 months ago

@spitters I only need to do the benchmarking, using make pretty-timed, but I have not figured out yet how to execute the benchmark for the made changes. Help with this is very welcome here.