[Ur] MySQL+InnoDB-backed sequences reset on database restart

[Adam Chlipala]

That's a local solution outside the Ur/Web implementation, but I'd still 
like to find a way to keep the semantics of Ur/Web sequences consistent 
across database backends.

On 06/14/2013 02:13 PM, Istvan Chung wrote:
> Well, another option could be to just maintain our own counter and
> increment it manually, forgoing AUTO_INCREMENT entirely.
>
> On 06/14/2013 01:07 PM, Adam Chlipala wrote:
>    
>> Wow, that's some grungy behavior on MySQL's part, which somehow doesn't
>> surprise me. :D
>>
>> It would certainly be an easy "fix" to remove the 'DELETE' command from
>> the Ur/Web compiler's handling of sequences in MySQL.  However, there
>> could be non-trivial performance consequences, as now an extra table
>> would exist with a row for every allocated sequence element.  Maybe
>> "real" rows using IDs are deleted periodically, so that the asymptotic
>> space usage of a database would increase under the proposed change.
>>
>> Does anyone have any ideas for a better way to implement Postgres-style
>> sequences in MySQL?  Alternatively, we could contemplate a compiler flag
>> to toggle MySQL behavior, giving an option to increase space use to make
>> the semantics nicer.  (It's not clear whether that option should be on
>> or off by default.)
>>
>> On 06/11/2013 11:23 PM, Istvan Chung wrote:
>>      
>>> It appears that when using MySQL with InnoDB, the AUTO_INCREMENT counter
>>> which Ur/Web uses to maintain sequences is reset when the database is
>>> restarted. This is because of a [bug in
>>> InnoDB](http://bugs.mysql.com/bug.php?id=199). In essence, whenever the
>>> database is restarted, InnoDB determines where the counter was left off
>>> by finding the first available number in each table which uses
>>> AUTO_INCREMENT, and uses that as the new initial value for the counter.
>>>
>>> However, since Ur/Web erases each entry in the table used to maintain
>>> the sequence as soon as it is done using that entry, InnoDB doesn't know
>>> which numbers have been used, and starts over at 1. Although this is a
>>> bug in InnoDB, it might be considered to simply remove (if only for
>>> MySQL+InnoDB) the behavior of erasing each entry as it is used, so that
>>> InnoDB can continue the AUTO_INCREMENT counter correctly.
>>>