uwplse / coq-change-analytics Goto Github PK
View Code? Open in Web Editor NEWREPLICA: REPL Instrumentation for Coq Analysis
License: GNU Lesser General Public License v2.1
REPLICA: REPL Instrumentation for Coq Analysis
License: GNU Lesser General Public License v2.1
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
:
coq-change-analytics/plugin/src/analytical.ml
Line 548 in 55dd66d
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
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
$ echo | coqtop
Welcome to Coq jgross-Leopard-WS:/home/jgross/Documents/repos/coq-change-analytics/plugin/coq,(HEAD detached at 5727443) (5727443376480be4793757fd5507621ad4f09509)
Coq < Coq <
$ git clean -xfd
$ ./build.sh
Thank you for installing Coq Change Analytics! We'll first install a few dependencies.
[NOTE] Package cohttp-lwt-unix is already installed (current version is 2.0.0).
[NOTE] Package cohttp is already installed (current version is 2.1.2).
[NOTE] Package sexplib is already installed (current version is v0.12.0).
Done. Now, to run this plugin, you need the latest Coq version (master). Do you already have this version of Coq installed? [y/n]
y
OK. We will build this plugin with your Coq version. First, let's generate a Makefile.
Done. From now on, run make in this directory to build the plugin.
$ make
COQDEP VFILES
COQPP src/analytical_plugin.mlg
COQDEP src/analytics.mlpack
CAMLDEP src/analytical.ml
CAMLDEP src/analytical_plugin.ml
CAMLOPT -c -for-pack Analytics src/analytical.ml
findlib: [WARNING] Interface redexpr.cmi occurs in several directories: /home/jgross/.local64/coq/coq-change-analytics/lib/coq/tactics, /home/jgross/.local64/coq/coq-change-analytics/lib/coq/proofs
findlib: [WARNING] Interface genredexpr.cmi occurs in several directories: /home/jgross/.local64/coq/coq-change-analytics/lib/coq/tactics, /home/jgross/.local64/coq/coq-change-analytics/lib/coq/interp
findlib: [WARNING] Interface redops.cmi occurs in several directories: /home/jgross/.local64/coq/coq-change-analytics/lib/coq/tactics, /home/jgross/.local64/coq/coq-change-analytics/lib/coq/interp
findlib: [WARNING] Interface loadpath.cmi occurs in several directories: /home/jgross/.local64/coq/coq-change-analytics/lib/coq/vernac, /home/jgross/.local64/coq/coq-change-analytics/lib/coq/library
File "src/analytical.ml", line 283, characters 32-47:
Error: Unbound module Float
Makefile:606: recipe for target 'src/analytical.cmx' failed
make[1]: *** [src/analytical.cmx] Error 2
Makefile:320: recipe for target 'all' failed
make: *** [all] Error 2
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.