uwplse / coq-change-analytics Goto Github PK

I'm always being asked to fill out a profile every time when running ./make and when loading the plugin (via coqtop I can see this happening, Proof General just hangs). I'm installing the plugin into user-contrib in a local Coq install pointed to Coq master (coq/coq@67c7c56).

See comments on #19

Using feedback from our own testing and the questions we choose, determine how to iterate on the logging information and format before the release.

Blocked by #8.

Think of concrete motivation for beta testers that we can act on when we try to distribute Beta. Drop ideas in here.

If I neglect to run coqtop from the command line before trying to use this plugin in emacs mode, it hangs emacs in an extremely unfriendly way. I have not found a way to recover except by quitting emacs, the plugin forces Coq to ignore the standard ways of killing coqtop (C-d) with "invalid input".

When a user first builds the plugin, prompt the user for his or her user type or expertise level. Save that and a persistent user ID across all sessions, and log it to the server.

I will fix this on Monday.

Determine whether the plugin works in Proof General right now, and if not, cut an issue to fix before Beta.

Distribute tool in opam, and separate the server from the client.

In particular, Stm.document_add_hook:

seems to be missing in coq-v8.9.1

Using feedback from Beta, determine how to iterate on the logging information and format before the release.

It seems that all that you're using Float for is Float.to_string, but you could just use Pervasives.string_of_float instead and not depend on OCaml 4.07. I'd prefer this, as I frequently switch between versions of Coq, and having them all built with the same OCaml is nice so I don't have to keep switching ocaml opam switches, and I'd like to not have to rebuild the dozen-or-so versions of Coq that I keep around.

See also #31

11: Start time: 2019-08-01 17:39:17.460000
12: Start time: 2019-08-01 17:40:59.350000
13: Start time: 2019-08-01 17:42:47.980000
Session #:13
Selected session (3, 1564681157.46)

This is properly a PG bug (reported as ProofGeneral/PG#422), but I think it might be faster to fix this on your side. I think the appropriate fix here is to update the submodule to point at coq/coq#8768 and update src/analytical.ml4 to work with coqpp (which will have to be done anyway in order to drop the submodule).

It looks like the upgrade will be quite straightforward: move everything except DECLARE PLUGIN "analytical" to a new file src/analytical.ml, then rename the file src/analytical.ml4 (containing only DECLARE PLUGIN "analytical") to src/analytical_plugin.mlg (you may also need to add

{

open Analytical

}

at the top?), add a line with Analytical_plugin to src/analytical.mlpack, and update _CoqProject appropriately.

Log to file on other hooks, and only send logs on exec, otherwise the tool hangs for large exec calls.

Draft out IRBs for UCSD and for UW before Beta. Determine whether we have enough information to submit before Beta, or whether we need to answer more questions using Beta. Plan accordingly.

If the user is using git, then log information about the git repository so that we have more information from which to reconstruct a session. If the user is not using git, then continue to function normally.

After upgrading coq to the master branch, I tried reinstalling for master and got the following error. (On running make, build.sh worked fine.)

CAMLOPT -pack -o src/analytics.cmx
File "src/analytics.cmx", line 1:
Error: src/consent.cmi is not a compiled interface for this version of OCaml.
It seems to be for an older version of OCaml.
make[1]: *** [src/analytics.cmx] Error 2
make: *** [all] Error 2

I'm using ocaml 4.08

In this issue, drop interesting questions that we might want to ask about the user data. Choose at least one and make sure we are logging enough information to answer it before releasing Beta.

I use a custom Makefile that doesn't build with -q, so the analytics plugin will be loaded during compilation as well as during interactive usage.

Is this bad for your data? If so, I can disable loading the rcfile in my various Makefiles. I'd sort of prefer to do so anyway since it would speed things up a bit.

$ git submodule update --init --recursive
fatal: reference is not a tree: 98d452051acbcef2744d7ff2a55f4b1b949d7a8e
Unable to checkout '98d452051acbcef2744d7ff2a55f4b1b949d7a8e' in submodule path 'coq'

I suspect this is because https://github.com/coq/coq/tree/98d452051acbcef2744d7ff2a55f4b1b949d7a8e is now an orphan and so is not fetched by git? But also this plugin does not build with the current version of coq/coq#8768 / https://github.com/ejgallego/coq/tree/stm+doc_hook:

$ coq_makefile -f _CoqProject CAMLPKGS = "-package cohttp -package cohttp-lwt-unix -package lwt" -o Makefile
camlp5 macro files not supported anymore, please port src/analytical.ml4 to coqpp

Write down any info you want about that Coq session to help reconstruct what was happening that we don't have in this issue, and we can use it to think of improvements before distributing.

Drop ideas in here, for now. We would like people of different user types and abilities as well as with different proof styles.

Once we're on master, we should probably just do this ASAP

• Notify beta testers and make sure that everyone removes their dependency on the plugin and their .analytics_profile
• Delete existing data (once we've played with analyzing it)
• Move on to next stage

See user 3, session 13, which should print "foo" before "bar" and "baz," for a test case of this.

The order changes when you have intermittent network outages, but the timestamps should always be correct.

This means that I have to do an enormous amount of manual setup for every single project I want to use this plugin with, as I have to manually copy (or symlink .analytics_profile) in every single subfolder of that project just to be able to start coqtop without it breaking PG due to #23

See comments on #19

Do failing tactics show up as distinguished in any way from tactics that go through? Do terms that don't type-check show up as distinguished in any way? We need to answer these questions.

If the answer to either of these is no, we should file another issue to access this information somehow, possibly before Beta (depending on the questions we ask) and possibly after.

Due to a Coq bug (coq/coq#10640), I get this printed out every time I compile a file with the plugin loaded via .coqrc:

R15:34 Analytical.Analytics <> <> lib

There doesn't seem to be a way to fix this, but I wanted to document it here in case anyone wondered where that was coming from.

Based on the data from the beta, it appears that most users are getting merged into the user "1", since there are 3983 sessions under user 1, and only 125 and 106 for users 2 and 3 respectively.