Switching default command history length from infinity to 1000

[olexandr-konovalov]

This is an alternative proposal to #958 which, instead of cleaning up the history just sets the default behaviour to keeping only last 1000 input lines.

[codecov-io]

Current coverage is 49.40% (diff: 100%)

Merging #960 into master will increase coverage by 0.01%

@@             master       #960   diff @@
==========================================
  Files           424        424          
  Lines        222804     222804          
  Methods        3430       3430          
  Messages          0          0          
  Branches          0          0          
==========================================
+ Hits         110042     110072    +30   
+ Misses       112762     112732    -30   
  Partials          0          0          

Powered by Codecov. Last update 9afb0fe...fc97b9a

[fingolfin]

This is fine by me.

[fingolfin]

Only question: Is 1000 a good default? Why not 10000? Of course in the end this is arbitrary no matter what... :-)

[olexandr-konovalov]

@fingolfin the default of 1000 was just taken from @vbraun's suggestion quoted in 958, and it seems to be the default value in Ubuntu (as I can see with echo $HISTSIZE on my desktop). So to me 1000 sounds fair enough, but if course I will be happy to increase this to say 10000 if someone thinks 1000 too small.

[james-d-mitchell]

1000 sounds good to me too

[ChrisJefferson]

I would like more than 1000, but then again I can always edit it myself.

Also setting it to 1000 makes it seem reasonable (to me) to then think about always turning on history loading/saving by default.

[olexandr-konovalov]

@ChrisJefferson wrote

Also setting it to 1000 makes it seem reasonable (to me) to then think about always turning on history loading/saving by default.

It's already on by default if the user has .gap directory and used WriteGapIniFile to create the default gap.ini file. I don't think we can do better - e.g. where to save the history if there is no .gap directory?

So I suggest to merge this PR as it is. Of course, @ChrisJefferson, if you'd be happier with 2000 lines, I can easily update the PR. Is there any particular context in which you may be interested in longer history, like e.g. interfacing GAP from another software?

[ChrisJefferson]

We could just make a .gap directory, and pop a default gap.ini file in there by default -- many applications do this kind of thing.

However, that's for another patch!