Skip to content

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

Draft
ndcroos wants to merge 5 commits into
rocq-community:masterfrom
ndcroos:master
Draft

Port Coq code to use 'done' tactic instead of 'easy' and benchmark#129
ndcroos wants to merge 5 commits into
rocq-community:masterfrom
ndcroos:master

Conversation

@ndcroos

@ndcroos ndcroos commented Jul 30, 2024

Copy link
Copy Markdown

@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
Copy Markdown
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

ndcroos commented Jul 30, 2024

Copy link
Copy Markdown
Author

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

Comment thread stdpp/stdpp_tactics.v Outdated
Comment thread stdpp/stdpp_tactics.v
Comment thread misc/util.v Outdated
@ndcroos

ndcroos commented Jul 31, 2024

Copy link
Copy Markdown
Author

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

ndcroos commented Jul 31, 2024

Copy link
Copy Markdown
Author

Files where replacing 'easy' didn't work:

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

@spitters

Copy link
Copy Markdown
Collaborator

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

@ndcroos

ndcroos commented Aug 14, 2024

Copy link
Copy Markdown
Author

@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