Skip to content
Snippets Groups Projects

Explicitly disable native compile

Closed Explicitly disable native compile
(removed):SkySkimmer-master-patch-11351 into master
Closed Gaëtan Gilbert requested to merge (removed):SkySkimmer-master-patch-11351 into master

Otherwise coq fails when compiled with native on because iris is compiled with native off

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
  • Ralf Jung
    Ralf Jung @jung
    Owner

    So... when a project uses native-compile no, then all their users also have to set that flag? That is surprising. In this case we probably want to remove this flag from Iris. Also the Coq docs need a big warning explaining this.

    Cc @robbertkrebbers

  • Ralf Jung
    Ralf Jung @jung
    Owner

    We're going to remove this flag from our _CoqProject files again, so this MR should not be needed.

  • Ralf Jung closed

    closed

Please register or sign in to reply