Skip to content

Conversation

@andres-erbsen
Copy link
Collaborator

Unfortunately on top of another PR.

set -e -u -x -o pipefail
mkdir subcomponents
 < .nix/rocq-overlays/stdlib-subcomponents/default.nix sed -n '/components =/,/"all"/p' | grep -v '= {' | tr -cd '[:alnum:].\n _-' | sed -e 's/\s\s*/ /g' -e 's/^ //g' | sed s/-/_/g | tee /dev/stderr | \
python -c '
import sys
for l in sys.stdin.read().splitlines():
    l = l.strip()
    if not l:
        continue
    comp, *subcomps = l.split()
    for sc in subcomps:
        with open(f"subcomponents/{comp}.v", "a") as myfile:
            myfile.write(f"From subcomponents Require {sc}.\n")
'

for f in theories/Make.* ; do \
	< "$f" grep 'v$' | \
	sed -e 's#/_\w\+##g' \
		-e 's#/#.#g' \
		-e 's/^\(.*\)\.v/From Stdlib Require \1./g' \
		>> "subcomponents/$(echo ${f#theories/Make.}.v | sed 's/-/_/g')" ; done
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.

1 participant