[search] [ssr] Emit deprecated message when calling search from ssreflect #12341
Conversation
ejgallego
added
kind: user messages
plugins/ssr/ssrvernac.mlg
Outdated
| "ssreflect Search command has been moved to the \ | ||
| ssrsearch module; please Require that module if you \ | ||
| still want to use ssreflect's Search command")) |
There was a problem hiding this comment.
Use official casing:
| "ssreflect Search command has been moved to the \ | |
| ssrsearch module; please Require that module if you \ | |
| still want to use ssreflect's Search command")) | |
| "SSReflect's Search command has been moved to the \ | |
| ssrsearch module; please Require that module if you \ | |
| still want to use SSReflect's Search command")) |
There was a problem hiding this comment.
I think the message should invite the user to try out the "vanilla" search and only require ssrsearch after filing an issue (of a missing feature for example).
The message assumes the user knows why the command was moved, which may not be the case.
There was a problem hiding this comment.
Note that the main reason for moving the command is because it overwrites the default one (see also #12253). The deprecation message emitted by Search in ssrsearch encourages the use of the default Search with the headconcl: clause instead.
There was a problem hiding this comment.
Oh, I see, the warning is implemented in ssr/ssrvernac.mlg but is only issues by ssrsearch/g_ssrsearch.mlg, am I right?
There was a problem hiding this comment.
There are two warnings:
- the one in ssrvernac is only emitted if the ssrsearch plugin is not loaded, and it tells the user that this is not anymore the SSReflect's
Search - the one in ssrsearch is emitted when using SSReflect's
Searchand recommends using theheadconcl:clause of the normalSearch.
Does that make sense? Would you do it differently?
There was a problem hiding this comment.
I have to try it out, I guess. I will before the final
|
The two refman failures are two unrelated timeouts. I think we were unlucky and got a sudden runner slowdown. This likely should go away at the next CI run. |
ejgallego
force-pushed
the
ssr+search_warn
branch
from
dceeabd
to
f076d9d
Compare
ejgallego
force-pushed
the
ssr+search_warn
branch
from
f076d9d
to
8c89cbc
Compare
plugins/ssr/ssrvernac.mlg
Outdated
|
|
||
| let warn_search_moved_enabled = ref true | ||
| let warn_search_moved = CWarnings.create ~name:"ssr-search-moved" | ||
| ~category:"deprecation" ~default:CWarnings.Enabled |
There was a problem hiding this comment.
Sorry for noticing that late, but this category does not exist. The following one does:
| ~category:"deprecation" ~default:CWarnings.Enabled | |
| ~category:"deprecated" ~default:CWarnings.Enabled |
There was a problem hiding this comment.
This is an area where we would IMHO gain from having a datatype + constructors.
There was a problem hiding this comment.
This is an area where we would IMHO gain from having a datatype + constructors.
Yes, I noticed this and I'm currently preparing a PR doing exactly this.
…lect but ssrsearch is not loaded. Fixes coq#12338
ejgallego
force-pushed
the
ssr+search_warn
branch
from
8c89cbc
to
57c023f
Compare
but ssrsearch is not loaded.
Fixes #12338
Actually I think it is a good idea to let this reach master for a while, for those using master + ssreflect.