On Thu, Sep 15, 2022 at 06:26:12PM +0200, Akim Demaille wrote: > Hi Frank, > > > Le 29 juil. 2022 à 14:09, Frank Heckenbach <[email protected]> a > > écrit : > > > > Hi, > > > > I don't know if it's something peculiar about my grammars, but it > > seems when using "-Wcounterexamples", Bison either finds > > counterexamples almost immediately or runs into the timeout. > > (Or maybe 6 seconds (see below) are just so eternally long to a > > modern CPU that there's not much between that and infinity. ;) > > [...] > > I agree. Let's change that. What do you think about this proposal?
I think the English text needs a few minor edits. > commit 6a15951030ade757de13159e545394af3cd40205 > Author: Akim Demaille <[email protected]> > Date: Tue Sep 13 08:25:59 2022 +0200 > > cex: provide the user with a means to change the timeout > > Reported by Frank Heckenbach. > https://lists.gnu.org/r/bug-bison/2022-07/msg00011.html > > * bootstrap.conf: Use c_strtod, so that even in French locales "1.5" > is accepted, instead of "1,5". > * src/counterexample.c, src/state-item.c: Use xtime_t instead of > time_t, so that accuracy goes from seconds to nanoseconds. > ( counterexample_init): Depend on cex.timeout rather than > $TIME_LIMIT. > * doc/bison.texi (%define Summary): Document cex.timeout. > > diff --git a/NEWS b/NEWS > index f480cb95..32e7361a 100644 > --- a/NEWS > +++ b/NEWS > @@ -8,6 +8,10 @@ GNU Bison NEWS > > The C++ skeletons now expose copy and move operators for symbols. > > + The `cex.timeout` %define variable allows to control when we give up > + finding a unifying counterexample. For instance `bison -Wcex > + -Dcex.timeout=.5 gram.y` to give 1/2s of credit. Is "credit" used this way elsewhere in the documentation? It feels like an unnatural usage to me. I'd either change it to "limit" (eg, "... to limit to 1/2s" or "... for a limit of 1/2s") or rephrase (eg, "... to stop after 1/2s"). [...] > +@c ================================================== cex.timeout > + > +@deffn Directive {%define cex.timeout} @var{duration} > + > +@itemize @bullet > +@item Language(s): all > + > +@item Purpose: > +Define the time credit allocated to finding unifying counterexamples. "Define the time limit for finding unifying counterexamples." [...] > diff --git a/src/muscle-tab.c b/src/muscle-tab.c > index 0945d609..40295542 100644 > --- a/src/muscle-tab.c > +++ b/src/muscle-tab.c > @@ -127,6 +127,9 @@ muscle_init (void) > > muscle_table = hash_xinitialize (HT_INITIAL_CAPACITY, NULL, hash_muscle, > hash_compare_muscles, muscle_entry_free); > + /* Avoid warnings if the user defined this variable, but did not > + actually called -Wcex. */ "actually use -Wcex" or "actually call with -Wcex". Be well, -- Jacob
