Skip to content

Ported plugin to Coq 8.13#43

Open
agrarpan wants to merge 44 commits into
uwplse:masterfrom
agrarpan:coq-8.13
Open

Ported plugin to Coq 8.13#43
agrarpan wants to merge 44 commits into
uwplse:masterfrom
agrarpan:coq-8.13

Conversation

@agrarpan
Copy link
Copy Markdown
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 added 13 commits October 25, 2023 18:23
@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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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