Skip to content

Share flags config by generating _CoqProject #285

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

Closed
rlepigre-skylabs-ai wants to merge 1 commit into from
Closed

Share flags config by generating _CoqProject #285

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,8 @@ bin
# generated by dune build -p
*.install

# Generated by dune
# Generated by the build system
theories/_CoqProject
_RocqProject

.dune-stamp
Expand Down
9 changes: 8 additions & 1 deletion theories/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,16 @@ ROCQMAKEOPTIONS?=
ROCQMAKEFILEOPTIONS?=

.PHONY: all install clean
all install clean: Makefile.coq
all install: Makefile.coq
+$(MAKE) -f $< $(ROCQMAKEOPTIONS) $@

clean: Makefile.coq
+$(MAKE) -f $< $(ROCQMAKEOPTIONS) $@
rm -f _CoqProject

_CoqProject: gen_CoqProject.sh rocq-flags.conf
./$< > $@

Makefile.coq: _CoqProject
$(ROCQMAKEFILE) $(ROCQMAKEFILEOPTIONS) -f $< $(shell find . -regex ".*/[^.][^/]*[.]v" -not -name All.v) -o $@

Expand Down
9 changes: 0 additions & 9 deletions theories/_CoqProject
View file
Open in desktop

This file was deleted.

14 changes: 8 additions & 6 deletions theories/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
(rule
(action
(with-stdout-to rocq-flags
(pipe-stdout
(cat rocq-flags.conf)
(bash "grep '^[^#]\\+' || true")))))

(include_subdirs qualified)
(rocq.theory
(name Stdlib)
(generate_project_file)
(flags :standard %{read-lines:rocq-flags})

@rlepigre-skylabs-ai rlepigre-skylabs-ai Jul 9, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

This enables the flag for all profiles instead of just the dev profile, but I guess that's fine right?

(package rocq-stdlib))

(env
(dev
(rocq
;; see theories/_CoqProject for details
(flags :standard -w -notation-for-abbreviation -w -ltac2-notation-for-abbreviation -w -implicit-create-hint-db -w -implicit-create-rewrite-hint-db -w -register-all -w -scheme-rewriting))))
14 changes: 14 additions & 0 deletions theories/gen_CoqProject.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
#!/bin/sh
set -e
# Script generating the contents of [_CoqProject] from [rocq-flags.conf].

echo "# Generated file, edit [gen_CoqProject.sh] / [rocq-flags.conf] instead."

echo
echo "# Search path"
echo "-R . Stdlib"

echo
echo "# Flags"
# Adding "-arg " prefix to all non-empty, non-comment lines of [config/flags].
cat rocq-flags.conf | grep "^[^#]\+" | sed "s/^/-arg /"
24 changes: 24 additions & 0 deletions theories/rocq-flags.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
# Specification for custom Rocq compilation flags.
# Syntax:
# - One flag per line with no leading/trailing blanks.
# - Empty lines and lines starting with '#' are ignored.

# Disable some warnings (for Rocq >= 9.2)

-w
-notation-for-abbreviation

-w
-ltac2-notation-for-abbreviation

-w
-implicit-create-hint-db

-w
-implicit-create-rewrite-hint-db

-w
-register-all

-w
-scheme-rewriting
Loading