Skip to content
Snippets Groups Projects

Rewrite create_makefile.sh as a Makefile

Merged Rewrite create_makefile.sh as a Makefile
proux1/rt-proofs:make_call_create into master
All threads resolved!
Merged Pierre Roux requested to merge proux1/rt-proofs:make_call_create into master
All threads resolved!

This simplifies the build process. We now only need to type make to launch the compilation, the Makefile will create the _CoqProject and Makefile.coq files itself.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Björn Brandenburg
    Björn Brandenburg @bbb ·
    Owner

    Looks good to me.

  • Pierre Roux resolved all threads

    resolved all threads

  • Pierre Roux added 1 commit

    added 1 commit

    • a12ab560 - Rewrite create_makefile.sh as a Makefile

    Compare with previous version

  • Pierre Roux resolved all threads

    resolved all threads

  • Björn Brandenburg added 2 commits

    added 2 commits

    • 7cb87380 - 1 commit from branch RT-PROOFS:master
    • 4eececb0 - Rewrite create_makefile.sh as a Makefile

    Compare with previous version

  • Björn Brandenburg enabled an automatic merge when the pipeline for 4eececb0 succeeds

    enabled an automatic merge when the pipeline for 4eececb0 succeeds

  • Björn Brandenburg merged

    merged

  • Björn Brandenburg
    Björn Brandenburg @bbb started a thread on commit 4eececb0
    • Makefile 0 → 100644
    42 refinementsCoqProject: commonCoqProject
    43 @echo "-R implementation/refinements prosa.implementation.refinements" >> $(COQ_PROJ)
    44 @echo "" >> $(COQ_PROJ)
    45 @find $(FIND_OPTS) \
    46 -path './implementation/refinements/*' \
    47 -print | scripts/module-toc-order.py >> $(COQ_PROJ)
    48
    49 $(COQ_MAKEFILE): $(COQ_PROJ) scripts/Makefile.coq.patch
    50 @coq_makefile -f $< -o $@
    51 @# Patch HTML target to switch out color, and
    52 @# so that it parses comments and has links to ssreflect.
    53 @# Also include Makefile.coqdocjs for 'htmlpretty' documentation target.
    54 @patch -s < scripts/Makefile.coq.patch
    55
    56 install html gallinahtml htmlpretty clean cleanall validate alectryon: $(COQ_MAKEFILE)
    57 $(MAKE) -f $(COQ_MAKEFILE) $@
    • Björn Brandenburg
      Björn Brandenburg @bbb ·
      Owner

      @proux — I just noticed this doesn't seem to pass on the -j option. As a result, it seems slow-but-parallelizable targets like alectryon don't benefit from multiple cores. Am I missing something?

    • Björn Brandenburg
      Björn Brandenburg @bbb ·
      Owner

      Mh, nevermind. I guess it's passed implicitly. At least it seems to work on my machine at home. It's just slow in CI.

    • Pierre Roux
      Pierre Roux @proux1 ·
      Author Developer

      Ok, my reading of GNU make documentation was indeed that $(MAKE) should pass the options directly without need for +$(MAKE).

    • Please register or sign in to reply
    Please register or sign in to reply