Skip to content
Snippets Groups Projects

Added strings to prelude to fix printing of strings.length

Merged Added strings to prelude to fix printing of strings.length
msammler/strings_in_prelude into master
2 unresolved threads
Merged Michael Sammler requested to merge msammler/strings_in_prelude into master
2 unresolved threads

This should hopefully fix strings.length showing up in random places. I tested it with iris and RefinedC. Both compile without changes and length is no more printed as strings.length in RefinedC. See the comment for the reasoning why I think this works.

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
theories/prelude.v
10 10 fin_sets
11 11 listset
12 12 list
13 (* This must be exported after base (which exports Coq.List) since
14 it exports the length notation to ensure that we use List.length and
15 not Strings.length. If we don't export strings here and some file
16 imports strings and then the prelude (which seems to happen with
17 Iris), the definition in Coq.List will shadow the notation in
  • Ralf Jung
    Ralf Jung @jung ·
    Owner

    Wouldn't it make more sense for Iris to import the prelude first?

  • Michael Sammler
    Michael Sammler @msammler ·
    Author Owner

    I don't know where strings gets imported in Iris. It can also be that something in iris exports the prelude, then strings and then the prelude again (this can easily happen because many files in iris export the prelude since it it exported transitively).

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Owner

    algebra/base.v exports prelude.

    There are a bunch of spurious exports of std.strings here and there, but probably all of those can be removed:

    $ mgrep std.*string
theories/proofmode/sel_patterns.v:From stdpp Require Export strings.
theories/proofmode/intro_patterns.v:From stdpp Require Export strings.
theories/proofmode/spec_patterns.v:From stdpp Require Export strings.
theories/proofmode/notation.v:From stdpp Require Export strings.
theories/proofmode/base.v:From stdpp Require Export strings.
theories/heap_lang/lang.v:From stdpp Require Export binders strings.
  • Please register or sign in to reply
  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers started a thread on the diff
    • theories/prelude.v
    10 10 fin_sets
    11 11 listset
    12 12 list
    13 (* This must be exported after base (which exports Coq.List) since
  • Michael Sammler
    Michael Sammler @msammler ·
    Author Owner

    Superseded by !129 (merged)

  • Michael Sammler closed

    closed

    • Please register or sign in to reply