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

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

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from

Conversation

ndcroos
Copy link

@ndcroos ndcroos commented Jul 30, 2024

@ndcroos ndcroos marked this pull request as draft July 30, 2024 16:08
@ndcroos ndcroos changed the title Replaced 'easy' tactic by 'done' Port Coq code to use 'done' tactic instead of 'easy' and benchmark Jul 30, 2024
@palmskog
Copy link
Member

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

ndcroos commented Jul 30, 2024

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

stdpp/stdpp_tactics.v Outdated Show resolved Hide resolved
stdpp/stdpp_tactics.v Outdated Show resolved Hide resolved
misc/util.v Outdated Show resolved Hide resolved
@ndcroos
Copy link
Author

ndcroos commented Jul 31, 2024

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

ndcroos commented Jul 31, 2024

Files where replacing 'easy' didn't work:

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

@spitters
Copy link
Collaborator

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

@ndcroos
Copy link
Author

ndcroos commented Aug 14, 2024

@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.

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

Successfully merging this pull request may close these issues.

3 participants