Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !491

add options file for library-wide configuration

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Ralf Jung requested to merge ralf/options-file into master Aug 12, 2020
  • Overview 14
  • Commits 6
  • Pipelines 0
  • Changes 143

This provides an easy way for us to set some Coq options in every file in Iris, without affecting user developments. For now we just do

Set Default Proof Using "Type".

but once we have this infrastructure, there might be more things we want to use it for.

This is not yet added to all files as I wanted to first solicit feedback. The following command prints the files that forget to import the options file:

for FILE in $(find theories/ -name "*.v" | fgrep -v theories/options.v); do if ! fgrep -q 'From iris Require Import options.' "$FILE"; then echo "$FILE"; fi done

We should probably check this to be empty on CI.

Fixes #66 (closed).

Edited Sep 05, 2020 by Ralf Jung
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ralf/options-file