Skip to content

feature(coq): coq macro#5967

Closed
Alizter wants to merge 1 commit intoocaml:mainfrom
Alizter:ps/rr/feature_coq___coq_config_macro
Closed

feature(coq): coq macro#5967
Alizter wants to merge 1 commit intoocaml:mainfrom
Alizter:ps/rr/feature_coq___coq_config_macro

Conversation

@Alizter
Copy link
Copy Markdown
Collaborator

@Alizter Alizter commented Jul 13, 2022 •
edited
Loading

We add an interface for the configuration values of Coq. This is important as it allows us to have version specific code. As a secondary we can expose it to users in their stanzas. We might want to cut down on the number however.

This adds a new %{coq:...} macro which lets you read the following:

The output of coqc --config:

%{coq:coqlib}
%{coq:coqcorelib}
%{coq:docdir}
%{coq:ocamlfind}
%{coq:camlflags}
%{coq:warn}
%{coq:hasnatdynlink}
%{coq:coq_src_subdirs}
%{coq:coq_native_compiler_default}

Version numbers for Coq:

%{coq:version}
%{coq:ocaml-version}
%{coq:version.major}
%{coq:version.minor}
%{coq:version.revision}
%{coq:version.suffix}

TODO:

  • Guard macro behind Coq lang
  • Doc

@Alizter Alizter marked this pull request as draft July 13, 2022 14:45
@Alizter Alizter force-pushed the ps/rr/feature_coq___coq_config_macro branch 3 times, most recently from 41732e9 to b5fc08c Compare July 13, 2022 21:23
@ejgallego
Copy link
Copy Markdown
Collaborator

ejgallego commented Jul 14, 2022

A lot of values there are for coq_makefile and will go away at some point to a coq-makefile specific tool. We should not include them.

@Alizter
Copy link
Copy Markdown
Collaborator Author

Alizter commented Jul 14, 2022 •
edited
Loading

Let's choose which ones then. I propose the following, you can edit as you see fit:

  • %{coq:coqlib}
  • %{coq:coqcorelib}
  • %{coq:docdir}
  • %{coq:ocamlfind}
  • %{coq:camlflags}
  • %{coq:warn}
  • %{coq:hasnatdynlink}
  • %{coq:coq_src_subdirs}
  • %{coq:coq_native_compiler_default}

The rest might be useless, but it is harmless to read them when they are available today. Even if they get removed in the future, it will allow Dune to understand configuration of Coq from previous versions etc.

@ejgallego
Copy link
Copy Markdown
Collaborator

ejgallego commented Jul 14, 2022 •
edited
Loading

Only two useful for us are coqlib and native compiler.

@Alizter
Copy link
Copy Markdown
Collaborator Author

Alizter commented Jul 14, 2022

@ejgallego We have access to all of them under the hood, so for "us" this doesn't matter. I'm talking about exposing them to the user, and I think something like %{docdir} might be useful?

@rgrinberg @Alizter
feature(coq): coq macro
9f0e5e1 
Signed-off-by: Ali Caglayan <alizter@gmail.com>

ps-id: fcb7d085-dc87-45a7-a37b-75ad0cd535c5
Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter force-pushed the ps/rr/feature_coq___coq_config_macro branch from b5fc08c to 9f0e5e1 Compare July 14, 2022 19:40
@ejgallego
Copy link
Copy Markdown
Collaborator

ejgallego commented Jul 26, 2022

I think that being conservative on what we expose will avoid any future problems. Why would docdir be useful?

Actually, while we need ourselves access to these variables to implement a few features, why would a user ever need access to these variables? Do we have use cases?

@Alizter
Copy link
Copy Markdown
Collaborator Author

Alizter commented Jul 31, 2022

OK I will restrict the available variables.

@Alizter Alizter mentioned this pull request Aug 7, 2022
Merged
@Alizter Alizter deleted the ps/rr/feature_coq___coq_config_macro branch October 26, 2022 18:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

Coq + Dune
Archived in project

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Alizter @ejgallego @rgrinberg