search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
351 stars 29 forks source link

Company Coq is sometimes noticeably laggy at obtaining symbols #131

Open JasonGross opened 8 years ago

JasonGross commented 8 years ago

Perhaps this is an instance of "doctor, it hurts when I poke myself". (This is in Coq 8.6)

Require Import Coq.btauto.Algebra Coq.btauto.Reflect Coq.btauto.Btauto Coq.derive.Derive Coq.extraction.ExtrHaskellBasic Coq.extraction.ExtrHaskellNatNum Coq.extraction.ExtrHaskellNatInt Coq.extraction.ExtrHaskellNatInteger Coq.extraction.ExtrHaskellZNum Coq.extraction.ExtrHaskellZInt Coq.extraction.ExtrHaskellZInteger Coq.extraction.ExtrHaskellString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlIntConv Coq.extraction.ExtrOcamlBigIntConv Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlZBigInt Coq.extraction.ExtrOcamlString Coq.fourier.Fourier_util Coq.fourier.Fourier Coq.funind.Recdef Coq.micromega.EnvRing Coq.micromega.Env Coq.micromega.OrderedRing Coq.micromega.Psatz Coq.micromega.QMicromega Coq.micromega.Refl Coq.micromega.RingMicromega Coq.micromega.RMicromega Coq.micromega.Tauto Coq.micromega.VarMap Coq.micromega.ZCoeff Coq.micromega.ZMicromega Coq.micromega.Lia Coq.nsatz.Nsatz Coq.omega.OmegaLemmas Coq.omega.OmegaPlugin Coq.omega.OmegaTactic Coq.omega.Omega Coq.omega.PreOmega Coq.quote.Quote Coq.romega.ReflOmegaCore Coq.romega.ROmega Coq.rtauto.Bintree Coq.rtauto.Rtauto Coq.setoid_ring.ArithRing Coq.setoid_ring.BinList Coq.setoid_ring.Field_tac Coq.setoid_ring.Field_theory Coq.setoid_ring.Field Coq.setoid_ring.InitialRing Coq.setoid_ring.NArithRing Coq.setoid_ring.RealField Coq.setoid_ring.Ring_base Coq.setoid_ring.Ring_polynom Coq.setoid_ring.Ring_tac Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring Coq.setoid_ring.ZArithRing Coq.setoid_ring.Algebra_syntax Coq.setoid_ring.Cring Coq.setoid_ring.Ncring Coq.setoid_ring.Ncring_polynom Coq.setoid_ring.Ncring_initial Coq.setoid_ring.Ncring_tac Coq.setoid_ring.Rings_Z Coq.setoid_ring.Rings_R Coq.setoid_ring.Rings_Q Coq.setoid_ring.Integral_domain Coq.ssrmatching.ssrmatching Coq.Arith.PeanoNat Coq.Arith.Arith_base Coq.Arith.Arith Coq.Arith.Between Coq.Arith.Bool_nat Coq.Arith.Compare_dec Coq.Arith.Compare Coq.Arith.Div2 Coq.Arith.EqNat Coq.Arith.Euclid Coq.Arith.Even Coq.Arith.Factorial Coq.Arith.Gt Coq.Arith.Le Coq.Arith.Lt Coq.Arith.Max Coq.Arith.Minus Coq.Arith.Min Coq.Arith.Mult Coq.Arith.Peano_dec Coq.Arith.Plus Coq.Arith.Wf_nat Coq.Bool.BoolEq Coq.Bool.Bool Coq.Bool.Bvector Coq.Bool.DecBool Coq.Bool.IfProp Coq.Bool.Sumbool Coq.Bool.Zerob Coq.Classes.DecidableClass Coq.Classes.Equivalence Coq.Classes.EquivDec Coq.Classes.Init Coq.Classes.Morphisms_Prop Coq.Classes.Morphisms_Relations Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Classes.SetoidClass Coq.Classes.SetoidDec Coq.Classes.SetoidTactics Coq.Classes.RelationPairs Coq.Classes.CRelationClasses Coq.Classes.CMorphisms Coq.Classes.CEquivalence Coq.Compat.AdmitAxiom Coq.Compat.Coq84 Coq.Compat.Coq85 Coq.Compat.Coq86 Coq.FSets.FMapAVL Coq.FSets.FMapFacts Coq.FSets.FMapFullAVL Coq.FSets.FMapInterface Coq.FSets.FMapList Coq.FSets.FMapPositive Coq.FSets.FMaps Coq.FSets.FMapWeakList Coq.FSets.FSetCompat Coq.FSets.FSetAVL Coq.FSets.FSetPositive Coq.FSets.FSetBridge Coq.FSets.FSetDecide Coq.FSets.FSetEqProperties Coq.FSets.FSetFacts Coq.FSets.FSetInterface Coq.FSets.FSetList Coq.FSets.FSetProperties Coq.FSets.FSets Coq.FSets.FSetToFiniteSet Coq.FSets.FSetWeakList Coq.Init.Datatypes Coq.Init.Logic_Type Coq.Init.Logic Coq.Init.Notations Coq.Init.Peano Coq.Init.Prelude Coq.Init.Specif Coq.Init.Tactics Coq.Init.Wf Coq.Init.Nat Coq.Init.Tauto Coq.Lists.ListSet Coq.Lists.ListTactics Coq.Lists.List Coq.Lists.ListDec Coq.Lists.SetoidList Coq.Lists.SetoidPermutation Coq.Lists.StreamMemo Coq.Lists.Streams Coq.Logic.Berardi Coq.Logic.ChoiceFacts Coq.Logic.ClassicalChoice Coq.Logic.ClassicalDescription Coq.Logic.ClassicalEpsilon Coq.Logic.ClassicalFacts Coq.Logic.Classical_Pred_Type Coq.Logic.Classical_Prop Coq.Logic.ClassicalUniqueChoice Coq.Logic.Classical Coq.Logic.ConstructiveEpsilon Coq.Logic.Decidable Coq.Logic.Description Coq.Logic.Diaconescu Coq.Logic.Epsilon Coq.Logic.Eqdep_dec Coq.Logic.EqdepFacts Coq.Logic.Eqdep Coq.Logic.WeakFan Coq.Logic.WKL Coq.Logic.FunctionalExtensionality Coq.Logic.ExtensionalityFacts Coq.Logic.Hurkens Coq.Logic.IndefiniteDescription Coq.Logic.JMeq Coq.Logic.ProofIrrelevanceFacts Coq.Logic.ProofIrrelevance Coq.Logic.RelationalChoice Coq.Logic.SetIsType Coq.Logic.FinFun Coq.MSets.MSetGenTree Coq.MSets.MSetAVL Coq.MSets.MSetRBT Coq.MSets.MSetDecide Coq.MSets.MSetEqProperties Coq.MSets.MSetFacts Coq.MSets.MSetInterface Coq.MSets.MSetList Coq.MSets.MSetProperties Coq.MSets.MSets Coq.MSets.MSetToFiniteSet Coq.MSets.MSetWeakList Coq.MSets.MSetPositive Coq.NArith.BinNatDef Coq.NArith.BinNat Coq.NArith.NArith Coq.NArith.Ndec Coq.NArith.Ndigits Coq.NArith.Ndist Coq.NArith.Nnat Coq.NArith.Ndiv_def Coq.NArith.Nsqrt_def Coq.NArith.Ngcd_def Coq.Numbers.BinNums Coq.Numbers.BigNumPrelude Coq.Numbers.Cyclic.Abstract.CyclicAxioms Coq.Numbers.Cyclic.Abstract.NZCyclic Coq.Numbers.Cyclic.DoubleCyclic.DoubleAdd Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1 Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv Coq.Numbers.Cyclic.DoubleCyclic.DoubleLift Coq.Numbers.Cyclic.DoubleCyclic.DoubleMul Coq.Numbers.Cyclic.DoubleCyclic.DoubleSqrt Coq.Numbers.Cyclic.DoubleCyclic.DoubleSub Coq.Numbers.Cyclic.DoubleCyclic.DoubleType Coq.Numbers.Cyclic.Int31.Int31 Coq.Numbers.Cyclic.Int31.Cyclic31 Coq.Numbers.Cyclic.Int31.Ring31 Coq.Numbers.Cyclic.ZModulo.ZModulo Coq.Numbers.Integer.Abstract.ZAddOrder Coq.Numbers.Integer.Abstract.ZAdd Coq.Numbers.Integer.Abstract.ZAxioms Coq.Numbers.Integer.Abstract.ZBase Coq.Numbers.Integer.Abstract.ZLt Coq.Numbers.Integer.Abstract.ZMulOrder Coq.Numbers.Integer.Abstract.ZMul Coq.Numbers.Integer.Abstract.ZSgnAbs Coq.Numbers.Integer.Abstract.ZDivFloor Coq.Numbers.Integer.Abstract.ZDivTrunc Coq.Numbers.Integer.Abstract.ZDivEucl Coq.Numbers.Integer.Abstract.ZMaxMin Coq.Numbers.Integer.Abstract.ZParity Coq.Numbers.Integer.Abstract.ZPow Coq.Numbers.Integer.Abstract.ZGcd Coq.Numbers.Integer.Abstract.ZLcm Coq.Numbers.Integer.Abstract.ZBits Coq.Numbers.Integer.Abstract.ZProperties Coq.Numbers.Integer.BigZ.BigZ Coq.Numbers.Integer.BigZ.ZMake Coq.Numbers.Integer.Binary.ZBinary Coq.Numbers.Integer.NatPairs.ZNatPairs Coq.Numbers.Integer.SpecViaZ.ZSig Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms Coq.Numbers.NaryFunctions Coq.Numbers.NatInt.NZAddOrder Coq.Numbers.NatInt.NZAdd Coq.Numbers.NatInt.NZAxioms Coq.Numbers.NatInt.NZBase Coq.Numbers.NatInt.NZMulOrder Coq.Numbers.NatInt.NZMul Coq.Numbers.NatInt.NZOrder Coq.Numbers.NatInt.NZProperties Coq.Numbers.NatInt.NZDomain Coq.Numbers.NatInt.NZParity Coq.Numbers.NatInt.NZDiv Coq.Numbers.NatInt.NZPow Coq.Numbers.NatInt.NZSqrt Coq.Numbers.NatInt.NZLog Coq.Numbers.NatInt.NZGcd Coq.Numbers.NatInt.NZBits Coq.Numbers.Natural.Abstract.NAddOrder Coq.Numbers.Natural.Abstract.NAdd Coq.Numbers.Natural.Abstract.NAxioms Coq.Numbers.Natural.Abstract.NBase Coq.Numbers.Natural.Abstract.NDefOps Coq.Numbers.Natural.Abstract.NIso Coq.Numbers.Natural.Abstract.NMulOrder Coq.Numbers.Natural.Abstract.NOrder Coq.Numbers.Natural.Abstract.NStrongRec Coq.Numbers.Natural.Abstract.NSub Coq.Numbers.Natural.Abstract.NProperties Coq.Numbers.Natural.Abstract.NDiv Coq.Numbers.Natural.Abstract.NMaxMin Coq.Numbers.Natural.Abstract.NParity Coq.Numbers.Natural.Abstract.NPow Coq.Numbers.Natural.Abstract.NSqrt Coq.Numbers.Natural.Abstract.NLog Coq.Numbers.Natural.Abstract.NGcd Coq.Numbers.Natural.Abstract.NLcm Coq.Numbers.Natural.Abstract.NBits Coq.Numbers.Natural.BigN.BigN Coq.Numbers.Natural.BigN.Nbasic Coq.Numbers.Natural.BigN.NMake_gen Coq.Numbers.Natural.BigN.NMake Coq.Numbers.Natural.Binary.NBinary Coq.Numbers.Natural.Peano.NPeano Coq.Numbers.Natural.SpecViaZ.NSigNAxioms Coq.Numbers.Natural.SpecViaZ.NSig Coq.Numbers.NumPrelude Coq.Numbers.Rational.BigQ.BigQ Coq.Numbers.Rational.BigQ.QMake Coq.Numbers.Rational.SpecViaQ.QSig Coq.PArith.BinPosDef Coq.PArith.BinPos Coq.PArith.Pnat Coq.PArith.POrderedType Coq.PArith.PArith Coq.Program.Basics Coq.Program.Combinators Coq.Program.Equality Coq.Program.Program Coq.Program.Subset Coq.Program.Syntax Coq.Program.Tactics Coq.Program.Utils Coq.Program.Wf Coq.QArith.Qabs Coq.QArith.QArith_base Coq.QArith.QArith Coq.QArith.Qcanon Coq.QArith.Qfield Coq.QArith.Qpower Coq.QArith.Qreals Coq.QArith.Qreduction Coq.QArith.Qring Coq.QArith.Qround Coq.QArith.QOrderedType Coq.QArith.Qminmax Coq.Reals.Alembert Coq.Reals.AltSeries Coq.Reals.ArithProp Coq.Reals.Binomial Coq.Reals.Cauchy_prod Coq.Reals.Cos_plus Coq.Reals.Cos_rel Coq.Reals.DiscrR Coq.Reals.Exp_prop Coq.Reals.Integration Coq.Reals.Machin Coq.Reals.MVT Coq.Reals.NewtonInt Coq.Reals.PartSum Coq.Reals.PSeries_reg Coq.Reals.Ranalysis1 Coq.Reals.Ranalysis2 Coq.Reals.Ranalysis3 Coq.Reals.Ranalysis4 Coq.Reals.Ranalysis5 Coq.Reals.Ranalysis Coq.Reals.Ranalysis_reg Coq.Reals.Ratan Coq.Reals.Raxioms Coq.Reals.Rbase Coq.Reals.Rbasic_fun Coq.Reals.Rcomplete Coq.Reals.Rdefinitions Coq.Reals.Rderiv Coq.Reals.Reals Coq.Reals.Rfunctions Coq.Reals.Rgeom Coq.Reals.RiemannInt_SF Coq.Reals.RiemannInt Coq.Reals.R_Ifp Coq.Reals.RIneq Coq.Reals.Rlimit Coq.Reals.RList Coq.Reals.Rlogic Coq.Reals.Rpow_def Coq.Reals.Rpower Coq.Reals.Rprod Coq.Reals.Rseries Coq.Reals.Rsigma Coq.Reals.Rsqrt_def Coq.Reals.R_sqrt Coq.Reals.R_sqr Coq.Reals.Rtopology Coq.Reals.Rtrigo_alt Coq.Reals.Rtrigo_calc Coq.Reals.Rtrigo_def Coq.Reals.Rtrigo_fun Coq.Reals.Rtrigo_reg Coq.Reals.Rtrigo1 Coq.Reals.Rtrigo Coq.Reals.SeqProp Coq.Reals.SeqSeries Coq.Reals.SplitAbsolu Coq.Reals.SplitRmult Coq.Reals.Sqrt_reg Coq.Reals.ROrderedType Coq.Reals.Rminmax Coq.Relations.Operators_Properties Coq.Relations.Relation_Definitions Coq.Relations.Relation_Operators Coq.Relations.Relations Coq.Setoids.Setoid Coq.Sets.Classical_sets Coq.Sets.Constructive_sets Coq.Sets.Cpo Coq.Sets.Ensembles Coq.Sets.Finite_sets_facts Coq.Sets.Finite_sets Coq.Sets.Image Coq.Sets.Infinite_sets Coq.Sets.Integers Coq.Sets.Multiset Coq.Sets.Partial_Order Coq.Sets.Permut Coq.Sets.Powerset_Classical_facts Coq.Sets.Powerset_facts Coq.Sets.Powerset Coq.Sets.Relations_1_facts Coq.Sets.Relations_1 Coq.Sets.Relations_2_facts Coq.Sets.Relations_2 Coq.Sets.Relations_3_facts Coq.Sets.Relations_3 Coq.Sets.Uniset Coq.Sorting.Heap Coq.Sorting.Permutation Coq.Sorting.PermutSetoid Coq.Sorting.PermutEq Coq.Sorting.Sorted Coq.Sorting.Sorting Coq.Sorting.Mergesort Coq.Strings.Ascii Coq.Strings.String Coq.Structures.Equalities Coq.Structures.EqualitiesFacts Coq.Structures.Orders Coq.Structures.OrdersEx Coq.Structures.OrdersFacts Coq.Structures.OrdersLists Coq.Structures.OrdersTac Coq.Structures.OrdersAlt Coq.Structures.GenericMinMax Coq.Structures.DecidableType Coq.Structures.DecidableTypeEx Coq.Structures.OrderedTypeAlt Coq.Structures.OrderedTypeEx Coq.Structures.OrderedType Coq.Unicode.Utf8 Coq.Unicode.Utf8_core Coq.Vectors.Fin Coq.Vectors.VectorDef Coq.Vectors.VectorSpec Coq.Vectors.VectorEq Coq.Vectors.Vector Coq.Wellfounded.Disjoint_Union Coq.Wellfounded.Inclusion Coq.Wellfounded.Inverse_Image Coq.Wellfounded.Lexicographic_Exponentiation Coq.Wellfounded.Lexicographic_Product Coq.Wellfounded.Transitive_Closure Coq.Wellfounded.Union Coq.Wellfounded.Wellfounded Coq.Wellfounded.Well_Ordering Coq.ZArith.auxiliary Coq.ZArith.BinIntDef Coq.ZArith.BinInt Coq.ZArith.Int Coq.ZArith.Wf_Z Coq.ZArith.Zabs Coq.ZArith.ZArith_base Coq.ZArith.ZArith_dec Coq.ZArith.ZArith Coq.ZArith.Zdigits Coq.ZArith.Zbool Coq.ZArith.Zcompare Coq.ZArith.Zcomplements Coq.ZArith.Zdiv Coq.ZArith.Zeven Coq.ZArith.Zgcd_alt Coq.ZArith.Zpow_alt Coq.ZArith.Zhints Coq.ZArith.Zlogarithm Coq.ZArith.Zmax Coq.ZArith.Zminmax Coq.ZArith.Zmin Coq.ZArith.Zmisc Coq.ZArith.Znat Coq.ZArith.Znumtheory Coq.ZArith.Zquot Coq.ZArith.Zorder Coq.ZArith.Zpow_def Coq.ZArith.Zpower Coq.ZArith.Zpow_facts Coq.ZArith.Zsqrt_compat Coq.ZArith.Zwf Coq.ZArith.Zeuclid.
Require Coq.QArith.Qcabs.
Set Search Output Name Only.
Time Redirect "/tmp/coq91756vir" SearchPattern _. (* Finished transaction in 0.228 secs (0.228u,0.s) (successful) *)
Time Redirect "/tmp/coq917568sx" SearchAbout -"____". (* Finished transaction in 0.278 secs (0.277u,0.s) (successful) *)
Remove Search Blacklist "Raw" "Proofs".
Unset Search Output Name Only.
JasonGross commented 7 years ago

This is kind-of important; I'm hitting this natively in Fiat. The timings for

Time Redirect "/tmp/coq266857Co" Print Ltac Signatures.
Time Redirect "/tmp/coq266857Co" Timeout 1 Print Grammar tactic.
Time Add Search Blacklist "Raw" "Proofs".
Time Set Search Output Name Only.
Time Redirect "/tmp/coq26685INu" SearchPattern _.
Time Redirect "/tmp/coq26685VX0" SearchAbout -"____".
Time Remove Search Blacklist "Raw" "Proofs".
Time Unset Search Output Name Only.

are:

Finished transaction in 0.003 secs (0.004u,0.s) (successful)
Finished transaction in 0.004 secs (0.004u,0.s) (successful)
Finished transaction in 0. secs (0.u,0.s) (successful)
Finished transaction in 0. secs (0.u,0.s) (successful)
Finished transaction in 0.139 secs (0.14u,0.s) (successful)
Finished transaction in 0.141 secs (0.132u,0.008s) (successful)
Remove Search Blacklist "Raw" "Proofs".
Finished transaction in 0. secs (0.u,0.s) (successful)

A quarter of a second is really noticeable and makes the entire experience feel sluggish, especially if I get it after every Ltac definition and things like idtac.

At the very least, can you make it so that rather than querying after each definition, you query in the background when the user starts typing something that might need to be autocompleted. (There are two requests here: (1) don't block the UI while querying these things and (2) only query if you haven't yet queried since the last evaluated sentence and also the user just typed a character that might feed into the autocompleter.)

jonleivent commented 7 years ago

I have noticed this lag, too - and it is annoying enough that I turn off Company-Coq mode at times just to eliminate it. If you can't easily eliminate it, is there a way to just turn off that part of Company-Coq?

cpitclaudel commented 7 years ago

At the very least, can you make it so that rather than querying after each definition, you query in the background when the user starts typing something that might need to be autocompleted.

No, I can't: what takes time is to process the large number of definitions that Coq is returning. I think I could make it a bit better, but the single-threadedness of Emacs Lisp will still bite us.

only query if you haven't yet queried since the last evaluated sentence and also the user just typed a character that might feed into the autocompleter.

I'm not sure. Do you think it would be better to block the UI while typing, rather than right after processing a definition?

cpitclaudel commented 7 years ago

If you can't easily eliminate it, is there a way to just turn off that part of Company-Coq?

Do you have the live-on-the-edge option on?

JasonGross commented 7 years ago

Do you have the live-on-the-edge option on?

No. Should I turn it on? The relevant bits of my ~/.emacs are:

(defun my-coq-hook ()
  (local-set-key (kbd "C-c RET") 'proof-goto-point)
  (set-input-method "Agda")
  (company-coq-initialize)
  (setq company-coq-extra-symbols-cmd "SearchAbout -\"____\"")
  (setq coq-end-goals-regexp-show-subgoals nil)
)

(add-hook 'coq-mode-hook 'my-coq-hook)

(global-set-key (kbd "C-c C-a C-u") #'company-coq-diff-unification-error)

(setq company-coq-dynamic-autocompletion t)

(add-hook 'company-coq-mode-hook
      (lambda ()
        (define-key company-coq-map (kbd "<backtab>") nil) ; disable collapsing on S-TAB
        (defconst company-coq-tg--preprocessor-substitutions
          '(("\n"  . " ") ("[ "  . "( OR-GROUP ") (" ]"  . " )")
        (" | " . " OR ") ("; "  . " AND ") ("'" . "’")))
        (define-key company-active-map [remap company-complete-common] #'company-indent-or-complete-common)))
(setq company-coq--use-special-set-unset-test-regexp t)

(setq company-coq-dynamic-autocompletion t)
JasonGross commented 7 years ago

Do you think it would be better to block the UI while typing, rather than right after processing a definition?

No. Can you set it up to block the UI only when the user hasn't given emacs any keyboard input for at least a second, and it's been at least a second since the last command finished processing. If the user hasn't paused in typing for a second and you need to give autocomplete feedback, display a warning in the status bar that says something like "Warning: Using outdated cached definitions for autocomplete. Press to refresh the autocomplete list." How does that sound? (You should probably make the 1 second timeout parameter tunable. If my characteristic frequency of keystroke is 1 second for some tasks, that come after evaluation, I'm going to be sad, and want to change the timeout to 2 seconds.) (Reasoning: Responsiveness is vastly more important to me than updated autocompletion. If I happen to need the particular autocomplete entry that is not in the cache because I've been typing too much without pause, I'm fine with waiting a second or pressing an extra key combo to update the cache.)

cpitclaudel commented 7 years ago

No. Should I turn it on? The relevant bits of my ~/.emacs are: (setq company-coq-dynamic-autocompletion t)

No; turning it off would help. That is, disabling dynamic autocompletion would help. These performance issues are the reason why I'm not graduating this to a by-default option :/

cpitclaudel commented 7 years ago

No. Can you set it up to block the UI only when the user hasn't given emacs any keyboard input for at least a second, and it's been at least a second since the last command finished processing.

I guess I could. I just need to find the time to implement it. But it's a bit tricky to get right: I need to find a time when it's safe to send input to Coqtop, and that's not trivial.

JasonGross commented 7 years ago

Can you set it up to block the UI only when the user hasn't given emacs any keyboard input

Note that something like this might already be implemented for code highlighting, I believe. If you stick a comment character in and keep typing, there's a delay before the color changes for the whole file, and it seems like it might be dependent on when you stop typing?

JasonGross commented 7 years ago

But it's a bit tricky to get right: I need to find a time when it's safe to send input to Coqtop, and that's not trivial.

How about this? Have a variable waiting-to-update-cache. When you send document stuff to Coq, set it to false. In the place where you currently send your extra commands, instead set it to true, and reset the timer. Any time the user sends keystrokes to emacs, reset the timer. When the timer goes off (a second later, or whatever), if waiting-to-update-cache is true, then query for the things you want.

cpitclaudel commented 7 years ago

That's not the issue. The issue is that there may already be a query in flight (from PG), and sending more stuff to Coq breaks everything in that case :/

cpitclaudel commented 7 years ago

Note that something like this might already be implemented for code highlighting, I believe

Yup, this is call idle timers in ELisp parlance :)

JasonGross commented 7 years ago

How does inline-docs (M-f12?) work without breaking everything, then?

JasonGross commented 6 years ago

@cpitclaudel poke This is still way too slow. I'm hitting cases where it takes > 9 seconds to fetch symbol data.

Somehow, when I do M-x company-coq-toggle-definition-overlay, company Coq gives me user-error: No information found for ‘make_Synthesis_package’. Try starting Coq, or waiting for processing to complete. (or similar) if and only if there's currently a command in flight. Any update on getting this implemented for symbol fetching? Evaluating to, e.g., line 5 of src/Specific/X25519/C64/Synthesis.v on branch zzz-slow-company-coq in my fork of fiat-crypto with Coq 8.7+beta1, I get

Time Redirect "c:/Users/Jason/AppData/Local/Temp/coq107449_m" Print Ltac Signatures. (* Finished transaction in 0.928 secs (0.u,0.s) (successful) *)
Time Print Grammar tactic. (* Finished transaction in 0.298 secs (0.u,0.s) (successful) *)
Time Add Search Blacklist "Raw" "Proofs". (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Set Search Output Name Only. (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Redirect "c:/Users/Jason/AppData/Local/Temp/coq10744KKt" SearchPattern _. (* Finished transaction in 9.191 secs (0.281u,0.062s) (successful) *)
Time Remove Search Blacklist "Raw" "Proofs". (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Unset Search Output Name Only. (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Print LoadPath. (* Finished transaction in 0.189 secs (0.u,0.s) (successful) *)
cpitclaudel commented 6 years ago

Sorry, this slid off my radar. But rereading through the thread, I'm confused. If symbol loading takes 9 seconds on your machine, why would launching the loading after a few seconds improve things? Instead of predictable 10-seconds freezes, you'd get 10-seconds unpredictable ones, right? Are you installing company-coq from source or from MELPA?

JasonGross commented 6 years ago

I believe my usage pattern is strongly clustered around a very short delay between commands, with a long tail. If 90% of the time that I edit a file within 2 minutes of my last keystroke‡, I edit it within 5 seconds of my last keystroke, then the right approximation here is to delay the autocompletion-launching for ~5 seconds. This way, I won't be bogged down by slowness 90% of the time. (The delay time should be settable in ~/.emacs.) Having emacs lag a bit when I've been spending the past 10 seconds trying to figure out what to do isn't that bad. Having emacs lag a lot between every single command execution makes coding unbearable.

Another optimization I'd like here is that company-coq fetching information from Coq should not prevent me from editing unlocked portions of the document, in the same way that telling PG to evaluate to a particular point doesn't prevent me from editing, even while Coq is spinning.

From MELPA.

‡ Actually "last keystroke" should be "the more recent of my last keystroke, and of Coq finishing execution of the document" ‎

cpitclaudel commented 6 years ago

Another optimization I'd like here is that company-coq fetching information from Coq should not prevent me from editing unlocked portions of the document, in the same way that telling PG to evaluate to a particular point doesn't prevent me from editing, even while Coq is spinning.

The problem is that we're running (synchronous) Lisp code, not waiting for Coq.

What about the following: if we detect a keystroke or something like that while fetching completions, we cancel the whole process and return control to you immediately. This just cancels the loading, essentially.

JasonGross commented 6 years ago

if we detect a keystroke or something like that while fetching completions, we cancel the whole process and return control to you immediately

Sounds good! (Assuming that emacs doesn't hang on trying to abort Coq's execution of the command (which it frequently does when I try to break, or tell it to quit Coq).)

cpitclaudel commented 6 years ago

Ok, I think I can look at this next week, when I come back to the US. Please remind me in person?

JasonGross commented 6 years ago

Thanks, will do

On Tue, Oct 10, 2017, 5:53 AM Clément Pit-Claudel notifications@github.com wrote:

Ok, I think I can look at this next week, when I come back to the US. Please remind me in person?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/company-coq/issues/131#issuecomment-335421845, or mute the thread https://github.com/notifications/unsubscribe-auth/AAYLLPgkx42u2MZYVjVyAU-Cl3dgL9VSks5sqz6LgaJpZM4Jn1Z8 .

JasonGross commented 6 years ago

Here are some backtraces: 1.

Debugger entered--Lisp error: (quit)
  redisplay_internal\ \(C\ function\)()

2.

company-coq: Loading symbols…
Error running timer `company-coq-maybe-reload-each': (error "Proof General: quit in proof-shell-wait")
Quit

3.

company-coq: Loading symbols…
Error running timer `company-coq-maybe-reload-each': (error "Proof General: quit in proof-shell-wait")
Quit

(There doesn't seem to really be a backtrace....)

cpitclaudel commented 6 years ago

Ah, snap. The backtraces you show are points during which PG is busy-waiting for Coq to finish writing out the list of all identifiers. I don't think there's a good way to interrupt this from company-coq, but it could be done from PG. Sounds tricky, though. Let's check: how long do each of the following Redirect commands take in one of your files?

Add Search Blacklist "Raw" "Proofs".
Set Search Output Name Only.
Redirect "/tmp/coq14243Gze" SearchPattern _.
Redirect "/tmp/coq14243T9k" SearchAbout -"____".
Remove Search Blacklist "Raw" "Proofs".
Unset Search Output Name Only.
JasonGross commented 6 years ago

In a file close to the end, but not at the end of the pipeline:

Time Add Search Blacklist "Raw" "Proofs". (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Set Search Output Name Only. (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Redirect "/tmp/coq14243Gze" SearchPattern _. (* Finished transaction in 1.321 secs (0.416u,0.011s) (successful) *) (* also, prints out 17502 lines of identifiers *)
Time Redirect "/tmp/coq14243T9k" SearchAbout -"____". (* Finished transaction in 0.985 secs (0.384u,0.016s) (successful) *) (* also prints out 17502 lines of identifiers *)
Time Remove Search Blacklist "Raw" "Proofs". (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
Time Unset Search Output Name Only. (* Finished transaction in 0. secs (0.u,0.s) (successful) *)

(I thought Redirect was supposed to write to a file instead of printing to output?)

cpitclaudel commented 6 years ago

(I thought Redirect was supposed to write to a file instead of printing to output?)

?! doesn't it? It does for me on 8.6...

cpitclaudel commented 6 years ago

Time Redirect "/tmp/coq14243Gze" SearchPattern _. ( Finished transaction in 1.321 secs (0.416u,0.011s) (successful) ) ( also, prints out 17502 lines of identifiers ) Time Redirect "/tmp/coq14243T9k" SearchAbout -"____". ( Finished transaction in 0.985 secs (0.384u,0.016s) (successful) ) ( also prints out 17502 lines of identifiers )

Hmm, still super long, then.

ejgallego commented 6 years ago

I think redirect is not working properly in 8.7, see coq/coq#6130 . It should be easy to fix.