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.

Sign up for GitHub

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

Jump to bottom

Ported plugin to Coq 8.13 #43

Open
wants to merge 44 commits into
base: master
Choose a base branch
from
Open

Ported plugin to Coq 8.13 #43

wants to merge 44 commits into from

Conversation

agrarpan
Copy link
Collaborator

@agrarpan agrarpan commented Jul 1, 2024

No description provided.

agrarpan and others added 30 commits July 20, 2023 16:55
@agrarpan
Move build to dune.
25b372f
@agrarpan
Fixed type errors, still some remaining.
60c6de8
@agrarpan
Fixed type errors, still some remaining.
6e33a0a
@agrarpan
Fixed type errors, still some remaining.
1ac2061
@agrarpan
Fixed type errors, still some remaining.
816cdee
@agrarpan
Fixed type errors, still some remaining.
858443e
@agrarpan
Fixed type errors, still some remaining.
19e5b26
@agrarpan
Undoing some changes from previous commit, using annotR uniformly now.
7f0c7ec
@agrarpan
Change typo in .gitignore
12f3ee5
@agrarpan
Remove unsused function.
1612ebc
@agrarpan
Renaming Globnames.global_reference to GlobRef.t
d8a0d14
@agrarpan
Fixed the type in indutils
e3076e5
@agrarpan
Fixed the type incompatibility in inference.ml
0ebe46b
@agrarpan
Refactored to maintain the original semantics.
fe44675
@agrarpan
Refactored constutils to handle type change of UnivGen.fresh_instance
eadbabf
@agrarpan
Refactored indutils to handle type changes to Declarations.universes
0b4e99f
@agrarpan
Refactored indutils to handle type changes to Declarations.universes
b1064b3
@agrarpan
Refactored defutils to handle type changes in Lemmas.hook_type
43813af
@agrarpan
Added mlg file
892b96c
@SkySkimmer @agrarpan
Merged changes from another fork branch to fix errors.
7836367
@agrarpan
Removed Makefile.local
b3cd62c
@agrarpan
Renamed plugin to match template, builds with dune currently.
55c3363
@agrarpan
Fixed warnings.
ffe7e16
@agrarpan
Fixed warnings.
b8af2c9
@agrarpan
Added error handling for SProp.
925fc08
@agrarpan
Changed the Context.binder_name usage to remove calls to annotR to ha…
9e874d3 
…ndle SProp correctly.
@agrarpan
Changed the Context.binder_name usage to remove calls to annotR to ha…
233f21d 
…ndle SProp correctly.
@agrarpan
Filter out SProp eliminators based on string match for sind.
7e47d4d
@agrarpan
Fixed bug that pushed the wrong name.
525f61e
@agrarpan
Changed the arguments to declare_structure to reflect the API change.
6607968
@agrarpan
Filter out SProp sorts to prevent call to Indrec.lookup_eliminator.
0082bd8
@agrarpan
Pulled in Max's changes from 8.11 branch of coq-plugin-lib
3a9de5d
@agrarpan
Made changes to the API to match Coq 8.12
0921f90
@agrarpan
Changed the cumulative flag to false to fix test errors in fix-to-elim
9fd5b6f
@agrarpan
First attempt at fixing declare_definition bug.
c1e4acd
@agrarpan
Passing false flag to EConstr.to_constr everywhere
fc53570
@agrarpan
Using declare_entry instead of declare_definition.
f063181
@agrarpan
Remove undefined evars before calling declare_definition.
603abcc
@agrarpan
Removed filter for sind.
35de5ad
@agrarpan
First batch of changes for coq 8.13
3ff1c96
@agrarpan
Removed the refresh flag from the define_term and define_canonical in…
25774f7 
…terfaces since we dont use the results anyway.
@agrarpan
Call Typing.type_of in case tyopt is not None.
642f7ba
@agrarpan
Preserve original typing call.
48a735a
tlringer
tlringer requested changes Jul 4, 2024
View reviewed changes
Copy link
Collaborator

@tlringer tlringer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good. What is the updated build process for all of this, especially for plugins that depend on it? If not done yet, please update the README with the updated build instructions.

@agrarpan
Copy link
Collaborator Author

agrarpan commented Jul 4, 2024

The build and test instructions are unchanged for all the plugins, although the build and testing scripts have been changed a little bit. Run ./build.sh to build the plugin (this will also pull in the correct dependencies).

@tlringer
Copy link
Collaborator

tlringer commented Jul 5, 2024

The build and test instructions are unchanged for all the plugins, although the build and testing scripts have been changed a little bit. Run ./build.sh to build the plugin (this will also pull in the correct dependencies).

It looks like the .build.sh file for the library was deleted, though, is that correct? How does one build just the library?

@tlringer
Copy link
Collaborator

tlringer commented Jul 5, 2024

If there's no more ./build.sh for the library, then please update the README appropriately with the updated build instructions for the library.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tlringer tlringer tlringer requested changes

Requested changes must be addressed to merge this pull request.

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@agrarpan @tlringer @SkySkimmer